--- a/src/HOL/Tools/Function/mutual.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/Function/mutual.ML Tue Mar 03 19:08:04 2015 +0100
@@ -209,7 +209,7 @@
fun mutual_induct_rules ctxt induct all_f_defs (Mutual {n, ST, parts, ...}) =
let
- val cert = cterm_of (Proof_Context.theory_of ctxt)
+ val cert = Proof_Context.cterm_of ctxt
val newPs =
map2 (fn Pname => fn MutualPart {cargTs, ...} =>
Free (Pname, cargTs ---> HOLogic.boolT))
@@ -259,7 +259,7 @@
val argsT = fastype_of (HOLogic.mk_tuple arg_vars)
val (args, name_ctxt) = mk_var "x" argsT name_ctxt
- val cert = cterm_of (Proof_Context.theory_of ctxt)
+ val cert = Proof_Context.cterm_of ctxt
val P = mk_var "P" @{typ "bool"} name_ctxt |> fst |> cert
val sumtree_inj = Sum_Tree.mk_inj ST n i args