1open HolKernel Parse boolLib 2 3open gh294aTheory gh294bTheory testutils 4 5val _ = new_theory "gh168c"; 6 7val tyg0 = type_grammar() 8val privthy = Binarymap.find(type_grammar.privileged_abbrevs tyg0, "foo") 9val unprivthy = if privthy = "gh294a" then "gh294b" else "gh294a" 10 11val _ = remove_type_abbrev (privthy ^ "$foo") 12 13val _ = tprint "foo abbrev no longer parses" 14val _ = (``:foo``; die "FAILED!") handle HOL_ERR _ => OK() 15 16fun typrinttest s expected = 17 let 18 val ty = Parse.Type [QUOTE s] 19 in 20 tprint (standard_tpp_message s); 21 if type_to_string ty = expected then OK() else die "FAILED!" 22 end 23 24val _ = typrinttest ":bool -> bool" 25 (if unprivthy = "gh294a" then ":gh294a$foo" 26 else ":bool -> bool") 27val _ = typrinttest ":bool -> bool -> bool" 28 (if unprivthy = "gh294a" then ":bool -> gh294a$foo" 29 else ":gh294b$foo") 30 31 32val _ = export_theory(); 33