1open HolKernel Parse boolLib
2
3open gh294aTheory gh294bTheory testutils
4
5val _ = new_theory "gh168e";
6
7val b2b = bool --> bool
8val b2b2b = bool --> b2b
9
10val tyg0 = type_grammar()
11val privthy = Binarymap.find(type_grammar.privileged_abbrevs tyg0, "foo")
12val unprivthy = if privthy = "gh294a" then "gh294b" else "gh294a"
13
14val (privty, unprivty) = if privthy = "gh294a" then (b2b, b2b2b)
15                         else (b2b2b, b2b)
16
17val ty = ``:foo``
18val _ = assert (equal privty) ty
19
20val _ = temp_thytype_abbrev ({Name = "foo", Thy = unprivthy}, unprivty)
21
22val ty = ``:foo``
23val _ = assert (equal unprivty) ty
24
25val _ = export_theory();
26