equal
deleted
inserted
replaced
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.transfer (Proof_Context.theory_of ctxt) |
47 |> Thm.transfer' ctxt |
48 |> Raw_Simplifier.norm_hhf_protect ctxt; |
48 |> Raw_Simplifier.norm_hhf_protect ctxt; |
49 val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt; |
49 val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt; |
50 val ((params, goal), ctxt2) = Variable.focus_cterm bindings (Thm.cprem_of st' i) ctxt1; |
50 val ((params, goal), ctxt2) = Variable.focus_cterm bindings (Thm.cprem_of st' i) ctxt1; |
51 |
51 |
52 val (asms, concl) = |
52 val (asms, concl) = |