Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
changeset 54883 dd04a8b654fc
parent 54844 630ba4d8a206
child 54899 7a01387c47d5 
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -1215,7 +1215,7 @@
 val add_primcorecursive_cmd = (fn (goalss, after_qed, lthy) =>
   lthy
   |> Proof.theorem NONE after_qed goalss
-  |> Proof.refine (Method.primitive_text I)
+  |> Proof.refine (Method.primitive_text (K I))
   |> Seq.hd) ooo add_primcorec_ursive_cmd NONE;
 
 val add_primcorec_cmd = (fn (goalss, after_qed, lthy) =>
isabelle