changeset 59580 | cbc38731d42f |
parent 59058 | a78612c67ec0 |
child 59582 | 0fbed69ff081 |
--- a/src/HOL/Tools/Function/induction_schema.ML Tue Mar 03 17:20:51 2015 +0100 +++ b/src/HOL/Tools/Function/induction_schema.ML Tue Mar 03 19:08:04 2015 +0100 @@ -354,7 +354,7 @@ val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt' val R = Free (Rn, mk_relT ST) val x = Free (xn, ST) - val cert = cterm_of (Proof_Context.theory_of ctxt) + val cert = Proof_Context.cterm_of ctxt val ineqss = mk_ineqs R scheme |> map (map (apply2 (Thm.assume o cert))) val complete =