equal
deleted
inserted
replaced
223 val cert = Thm.cterm_of thy; |
223 val cert = Thm.cterm_of thy; |
224 |
224 |
225 val th = MetaSimplifier.norm_hhf raw_th; |
225 val th = MetaSimplifier.norm_hhf raw_th; |
226 val is_elim = ObjectLogic.is_elim th; |
226 val is_elim = ObjectLogic.is_elim th; |
227 |
227 |
228 val ((_, [th']), ctxt') = Variable.import_thms true [th] (Variable.set_body false ctxt); |
228 val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body false ctxt); |
229 val prop = Thm.prop_of th'; |
229 val prop = Thm.prop_of th'; |
230 val (prems, concl) = Logic.strip_horn prop; |
230 val (prems, concl) = Logic.strip_horn prop; |
231 val concl_term = ObjectLogic.drop_judgment thy concl; |
231 val concl_term = ObjectLogic.drop_judgment thy concl; |
232 |
232 |
233 val fixes = fold_aterms (fn v as Free (x, T) => |
233 val fixes = fold_aterms (fn v as Free (x, T) => |