Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
replaced Conv.goals_conv by Conv.prems_conv;
authorwenzelm
Tue, 03 Jul 2007 17:17:16 +0200
changeset 23542 61ffcf4c02c7
parent 23541 f8c5e218e4d8
child 23543 12271cfad085
replaced Conv.goals_conv by Conv.prems_conv;
src/Pure/Isar/rule_cases.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/rule_cases.ML	Tue Jul 03 17:17:15 2007 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Tue Jul 03 17:17:16 2007 +0200
@@ -189,7 +189,7 @@
 
 fun unfold_prems n defs th =
   if null defs then th
-  else Conv.fconv_rule (Conv.goals_conv (fn i => i <= n) (MetaSimplifier.rewrite true defs)) th;
+  else Conv.fconv_rule (Conv.prems_conv n (K (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
isabelle