equal
deleted
inserted
replaced
134 val thm = |
134 val thm = |
135 (case program of |
135 (case program of |
136 NONE => @{thm refl} |
136 NONE => @{thm refl} |
137 | SOME a => Global_Theory.get_thm thy (Global_Theory.check_fact thy a)); |
137 | SOME a => Global_Theory.get_thm thy (Global_Theory.check_fact thy a)); |
138 val arg = prep_input thy name maa id_empty (metID, model_input, input, thm); |
138 val arg = prep_input thy name maa id_empty (metID, model_input, input, thm); |
139 in KEStore_Elems.add_mets [arg] thy end))) |
139 in KEStore_Elems.add_mets @{context} [arg] thy end))) |
140 |
140 |
141 in end; |
141 in end; |
142 |
142 |
143 (** get MethodC from Store **) |
143 (** get MethodC from Store **) |
144 |
144 |