src/Pure/Isar/subgoal.ML
changeset 71945 8ed68b2aeba1
parent 67721 5348bea4accd
child 74501 c49134ee16c1
equal deleted inserted replaced
71880:9fdbd2f0b56e 71945:8ed68b2aeba1
    42   concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list};
    42   concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list};
    43 
    43 
    44 fun gen_focus (do_prems, do_concl) ctxt i bindings raw_st =
    44 fun gen_focus (do_prems, do_concl) ctxt i bindings raw_st =
    45   let
    45   let
    46     val st = raw_st
    46     val st = raw_st
       
    47       |> Thm.solve_constraints
    47       |> Thm.transfer' ctxt
    48       |> Thm.transfer' ctxt
    48       |> Raw_Simplifier.norm_hhf_protect ctxt;
    49       |> Raw_Simplifier.norm_hhf_protect ctxt;
    49     val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
    50     val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
    50     val ((params, goal), ctxt2) = Variable.focus_cterm bindings (Thm.cprem_of st' i) ctxt1;
    51     val ((params, goal), ctxt2) = Variable.focus_cterm bindings (Thm.cprem_of st' i) ctxt1;
    51 
    52