src/ZF/Tools/primrec_package.ML
changeset 54742 7a86358a3c0b
parent 51930 52fd62618631
child 58011 bc6bced136e5
     1.1 --- a/src/ZF/Tools/primrec_package.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/ZF/Tools/primrec_package.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -176,7 +176,7 @@
     1.4      val eqn_thms =
     1.5        eqn_terms |> map (fn t =>
     1.6          Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t)
     1.7 -          (fn _ => EVERY [rewrite_goals_tac rewrites, rtac @{thm refl} 1]));
     1.8 +          (fn {context = ctxt, ...} => EVERY [rewrite_goals_tac ctxt rewrites, rtac @{thm refl} 1]));
     1.9  
    1.10      val (eqn_thms', thy2) =
    1.11        thy1