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