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/Isar/rule_cases.ML
changeset 23584 9b5ba76de1c2
parent 23542 61ffcf4c02c7
child 23657 2332c79f4dc8 
--- a/src/Pure/Isar/rule_cases.ML	Thu Jul 05 00:06:22 2007 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Thu Jul 05 00:06:23 2007 +0200
@@ -189,14 +189,14 @@
 
 fun unfold_prems n defs th =
   if null defs then th
-  else Conv.fconv_rule (Conv.prems_conv n (K (MetaSimplifier.rewrite true defs))) th;
+  else Conv.fconv_rule (Conv.prems_conv n (MetaSimplifier.rewrite true defs)) th;
 
 fun unfold_prems_concls defs th =
   if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
   else
     Conv.fconv_rule
       (Conv.concl_conv ~1 (Conjunction.convs
-        (Conv.prems_conv ~1 (K (MetaSimplifier.rewrite true defs))))) th;
+        (Conv.prems_conv ~1 (MetaSimplifier.rewrite true defs)))) th;
 
 in
isabelle