1open HolKernel Parse boolLib 2 3open gh294aTheory gh294bTheory testutils 4 5val _ = new_theory "gh168b"; 6 7val _ = remove_type_abbrev "foo" 8 9val tyg = type_grammar() 10 11val _ = tprint "foo abbrev no longer parses" 12val _ = (``:foo``; die "FAILED!") handle HOL_ERR _ => OK() 13 14fun typrinttest s = 15 let 16 val ty = Parse.Type [QUOTE s] 17 in 18 tprint (standard_tpp_message s); 19 if s = type_to_string ty then OK() else die "FAILED!" 20 end 21 22val _ = typrinttest ":bool -> bool" 23val _ = typrinttest ":bool -> bool -> bool" 24val _ = tprint "type_grammar abbrevs map is empty" 25val _ = if Binarymap.numItems (type_grammar.parse_map tyg) = 4 then OK() 26 else die "FAILED!" 27 28val _ = export_theory(); 29