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/Pure/thm.ML
changeset 36742 6f8bbe9ca8a2
parent 36621 2fd4e2c76636
child 36744 6e1f3d609a68 
--- a/src/Pure/thm.ML	Sat May 08 16:03:09 2010 +0200
+++ b/src/Pure/thm.ML	Sat May 08 16:24:44 2010 +0200
@@ -1436,7 +1436,7 @@
         in Logic.list_implies (fixed_prems @ qs @ ps, concl) end
       else raise THM ("permute_prems: k", k, [rl]);
   in
-    Thm (deriv_rule1 (Pt.permute_prems_prf prems j m) der,
+    Thm (deriv_rule1 (Pt.permute_prems_proof prems j m) der,
      {thy_ref = thy_ref,
       tags = [],
       maxidx = maxidx,
isabelle