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