src/Tools/induct.ML
changeset 59621 291934bac95e
parent 59586 ddf6deaadfe8
child 59843 b640b5e6b023
     1.1 --- a/src/Tools/induct.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/Tools/induct.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -162,7 +162,7 @@
     1.4  
     1.5  val rearrange_eqs_simproc =
     1.6    Simplifier.simproc_global Pure.thy "rearrange_eqs" ["Pure.all t"]
     1.7 -    (fn ctxt => fn t => mk_swap_rrule ctxt (Thm.cterm_of (Proof_Context.theory_of ctxt) t));
     1.8 +    (fn ctxt => fn t => mk_swap_rrule ctxt (Thm.global_cterm_of (Proof_Context.theory_of ctxt) t));
     1.9  
    1.10  
    1.11  (* rotate k premises to the left by j, skipping over first j premises *)
    1.12 @@ -394,7 +394,7 @@
    1.13  
    1.14  fun prep_inst ctxt align tune (tm, ts) =
    1.15    let
    1.16 -    val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
    1.17 +    val cert = Thm.global_cterm_of (Proof_Context.theory_of ctxt);
    1.18      fun prep_var (x, SOME t) =
    1.19            let
    1.20              val cx = cert x;
    1.21 @@ -571,8 +571,8 @@
    1.22  
    1.23  fun dest_env thy env =
    1.24    let
    1.25 -    val cert = Thm.cterm_of thy;
    1.26 -    val certT = Thm.ctyp_of thy;
    1.27 +    val cert = Thm.global_cterm_of thy;
    1.28 +    val certT = Thm.global_ctyp_of thy;
    1.29      val pairs = Vartab.dest (Envir.term_env env);
    1.30      val types = Vartab.dest (Envir.type_env env);
    1.31      val ts = map (cert o Envir.norm_term env o #2 o #2) pairs;
    1.32 @@ -655,7 +655,7 @@
    1.33  fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) =>
    1.34    let
    1.35      val thy = Proof_Context.theory_of ctxt;
    1.36 -    val cert = Thm.cterm_of thy;
    1.37 +    val cert = Thm.global_cterm_of thy;
    1.38  
    1.39      val v = Free (x, T);
    1.40      fun spec_rule prfx (xs, body) =