76 |
76 |
77 val token_markers = |
77 val token_markers = |
78 ["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"]; |
78 ["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"]; |
79 |
79 |
80 val _ = Theory.setup |
80 val _ = Theory.setup |
81 (Sign.map_naming (Name_Space.set_theory_name Context.PureN) #> |
81 (Sign.theory_naming #> |
82 Old_Appl_Syntax.put false #> |
82 Old_Appl_Syntax.put false #> |
83 Sign.add_types_global |
83 Sign.add_types_global |
84 [(Binding.make ("fun", \<^here>), 2, NoSyn), |
84 [(Binding.make ("fun", \<^here>), 2, NoSyn), |
85 (Binding.make ("prop", \<^here>), 0, NoSyn), |
85 (Binding.make ("prop", \<^here>), 0, NoSyn), |
86 (Binding.make ("itself", \<^here>), 1, NoSyn), |
86 (Binding.make ("itself", \<^here>), 1, NoSyn), |