--- a/src/HOL/Tools/Function/partial_function.ML Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML Fri Mar 06 15:58:56 2015 +0100
@@ -113,7 +113,7 @@
let
val thy = Thm.theory_of_thm thm;
val vs = rev (Term.add_vars (Thm.prop_of thm) [])
- |> map (Thm.cterm_of thy o Var);
+ |> map (Thm.global_cterm_of thy o Var);
in
cterm_instantiate (zip_options vs cts) thm
end;
@@ -168,7 +168,7 @@
curry induction predicate *)
fun specialize_fixp_induct ctxt args fT fT_uc F curry uncurry mono_thm f_def rule =
let
- val cert = Proof_Context.cterm_of ctxt
+ val cert = Thm.cterm_of ctxt
val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt
val P_inst = Abs ("f", fT_uc, Free (P, fT --> HOLogic.boolT) $ (curry $ Bound 0))
in
@@ -187,7 +187,7 @@
fun mk_curried_induct args ctxt inst_rule =
let
- val cert = Proof_Context.cterm_of ctxt
+ val cert = Thm.cterm_of ctxt
val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt
val split_paired_all_conv =
@@ -234,7 +234,7 @@
val ((f_binding, fT), mixfix) = the_single fixes;
val fname = Binding.name_of f_binding;
- val cert = Proof_Context.cterm_of lthy;
+ val cert = Thm.cterm_of lthy;
val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop plain_eqn);
val (head, args) = strip_comb lhs;
val argnames = map (fst o dest_Free) args;