equal
deleted
inserted
replaced
81 fun process_spec cos alt_props thy = |
81 fun process_spec cos alt_props thy = |
82 let |
82 let |
83 val ctxt = Proof_Context.init_global thy |
83 val ctxt = Proof_Context.init_global thy |
84 |
84 |
85 val rew_imps = alt_props |> |
85 val rew_imps = alt_props |> |
86 map (Object_Logic.atomize ctxt o Thm.global_cterm_of thy o Syntax.read_prop_global thy o snd) |
86 map (Object_Logic.atomize ctxt o Thm.cterm_of ctxt o Syntax.read_prop_global thy o snd) |
87 val props' = rew_imps |> |
87 val props' = rew_imps |> |
88 map (HOLogic.dest_Trueprop o Thm.term_of o snd o Thm.dest_equals o Thm.cprop_of) |
88 map (HOLogic.dest_Trueprop o Thm.term_of o snd o Thm.dest_equals o Thm.cprop_of) |
89 |
89 |
90 fun proc_single prop = |
90 fun proc_single prop = |
91 let |
91 let |