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