src/HOL/Nominal/nominal_fresh_fun.ML
changeset 58956 a816aa3ff391
parent 58950 d07464875dd4
child 59058 a78612c67ec0
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Sun Nov 09 11:05:20 2014 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sun Nov 09 14:08:00 2014 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  (* FIXME res_inst_tac mostly obsolete, cf. Subgoal.FOCUS *)
     1.5  
     1.6  (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
     1.7 -fun gen_res_inst_tac_term instf tyinst tinst elim th i st =
     1.8 +fun gen_res_inst_tac_term ctxt instf tyinst tinst elim th i st =
     1.9    let
    1.10      val thy = theory_of_thm st;
    1.11      val cgoal = nth (cprems_of st) (i - 1);
    1.12 @@ -27,18 +27,18 @@
    1.13        (map (pairself (cterm_of thy)) tinst')
    1.14        (Thm.lift_rule cgoal th)
    1.15    in
    1.16 -    compose_tac (elim, th', nprems_of th) i st
    1.17 +    compose_tac ctxt (elim, th', nprems_of th) i st
    1.18    end handle General.Subscript => Seq.empty;
    1.19  (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
    1.20  
    1.21 -val res_inst_tac_term =
    1.22 -  gen_res_inst_tac_term (curry Thm.instantiate);
    1.23 +fun res_inst_tac_term ctxt =
    1.24 +  gen_res_inst_tac_term ctxt (curry Thm.instantiate);
    1.25  
    1.26 -val res_inst_tac_term' =
    1.27 -  gen_res_inst_tac_term (K Drule.cterm_instantiate) [];
    1.28 +fun res_inst_tac_term' ctxt =
    1.29 +  gen_res_inst_tac_term ctxt (K Drule.cterm_instantiate) [];
    1.30  
    1.31  fun cut_inst_tac_term' ctxt tinst th =
    1.32 -  res_inst_tac_term' tinst false (Rule_Insts.make_elim_preserve ctxt th);
    1.33 +  res_inst_tac_term' ctxt tinst false (Rule_Insts.make_elim_preserve ctxt th);
    1.34  
    1.35  fun get_dyn_thm thy name atom_name =
    1.36    Global_Theory.get_thm thy name handle ERROR _ =>