equal
deleted
inserted
replaced
113 fun add_def theory = |
113 fun add_def theory = |
114 if def then |
114 if def then |
115 theory |
115 theory |
116 |> Sign.add_consts_i [(name, setT', NoSyn)] |
116 |> Sign.add_consts_i [(name, setT', NoSyn)] |
117 |> PureThy.add_defs false [Thm.no_attributes (apfst (Binding.name) |
117 |> PureThy.add_defs false [Thm.no_attributes (apfst (Binding.name) |
118 (PrimitiveDefs.mk_defpair (setC, set)))] |
118 (Primitive_Defs.mk_defpair (setC, set)))] |
119 |-> (fn [th] => pair (SOME th)) |
119 |-> (fn [th] => pair (SOME th)) |
120 else (NONE, theory); |
120 else (NONE, theory); |
121 fun contract_def NONE th = th |
121 fun contract_def NONE th = th |
122 | contract_def (SOME def_eq) th = |
122 | contract_def (SOME def_eq) th = |
123 let |
123 let |