equal
deleted
inserted
replaced
279 |
279 |
280 val lhs' = Morphism.term (Local_Theory.target_morphism lthy5) lhs; |
280 val lhs' = Morphism.term (Local_Theory.target_morphism lthy5) lhs; |
281 |
281 |
282 val _ = |
282 val _ = |
283 Proof_Display.print_consts int (Position.thread_data ()) lthy5 |
283 Proof_Display.print_consts int (Position.thread_data ()) lthy5 |
284 (member (op =) (Term.add_frees lhs' [])) [(x, T)]; |
284 (Term_Subst.Frees.defined (Term_Subst.add_frees lhs' Term_Subst.Frees.empty)) [(x, T)]; |
285 in ((lhs, (def_name, th')), lthy5) end; |
285 in ((lhs, (def_name, th')), lthy5) end; |
286 |
286 |
287 val definition' = gen_def check_spec_open (K I); |
287 val definition' = gen_def check_spec_open (K I); |
288 fun definition xs ys As B = definition' xs ys As B false; |
288 fun definition xs ys As B = definition' xs ys As B false; |
289 val definition_cmd = gen_def read_spec_open Attrib.check_src; |
289 val definition_cmd = gen_def read_spec_open Attrib.check_src; |