src/Pure/Isar/subgoal.ML
changeset 74501 c49134ee16c1
parent 71945 8ed68b2aeba1
child 74567 d637611b41bd
equal deleted inserted replaced
74500:1d25be2353e1 74501:c49134ee16c1
    53     val (asms, concl) =
    53     val (asms, concl) =
    54       if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
    54       if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
    55       else ([], goal);
    55       else ([], goal);
    56     val text = asms @ (if do_concl then [concl] else []);
    56     val text = asms @ (if do_concl then [concl] else []);
    57 
    57 
    58     val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
    58     val ((_, inst), ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
    59     val schematic_terms = map (apsnd (Thm.cterm_of ctxt3)) (#2 inst);
    59     val schematic_terms = Term_Subst.Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt3 t)) inst [];
    60 
    60 
    61     val schematics = (schematic_types, schematic_terms);
    61     val schematics = (schematic_types, schematic_terms);
    62     val asms' = map (Thm.instantiate_cterm schematics) asms;
    62     val asms' = map (Thm.instantiate_cterm schematics) asms;
    63     val concl' = Thm.instantiate_cterm schematics concl;
    63     val concl' = Thm.instantiate_cterm schematics concl;
    64     val (prems, context) = Assumption.add_assumes asms' ctxt3;
    64     val (prems, context) = Assumption.add_assumes asms' ctxt3;