src/ZF/Tools/primrec_package.ML
changeset 58838 59203adfc33f
parent 58011 bc6bced136e5
child 59498 50b60f501b05
     1.1 --- a/src/ZF/Tools/primrec_package.ML	Thu Oct 30 16:20:46 2014 +0100
     1.2 +++ b/src/ZF/Tools/primrec_package.ML	Thu Oct 30 16:55:29 2014 +0100
     1.3 @@ -176,7 +176,8 @@
     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 {context = ctxt, ...} => EVERY [rewrite_goals_tac ctxt rewrites, rtac @{thm refl} 1]));
     1.8 +          (fn {context = ctxt, ...} =>
     1.9 +            EVERY [rewrite_goals_tac ctxt rewrites, resolve_tac @{thms refl} 1]));
    1.10  
    1.11      val (eqn_thms', thy2) =
    1.12        thy1