# HG changeset patch
# User wenzelm
# Date 1183586783 -7200
# Node ID 9b5ba76de1c20e206ec3112121cdb606661f94f2
# Parent  00751df1f98c407bf4a620dd10a3f834d0cd3333
tuned goal conversion interfaces;

diff -r 00751df1f98c -r 9b5ba76de1c2 src/Pure/Isar/rule_cases.ML
--- 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
 
diff -r 00751df1f98c -r 9b5ba76de1c2 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Thu Jul 05 00:06:22 2007 +0200
+++ b/src/Pure/meta_simplifier.ML	Thu Jul 05 00:06:23 2007 +0200
@@ -1271,13 +1271,13 @@
 
 (*Rewrite the subgoals of a proof state (represented by a theorem)*)
 fun rewrite_goals_rule thms th =
-  Conv.fconv_rule (Conv.prems_conv ~1 (K (rewrite_cterm (true, true, true) simple_prover
-    (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms)))) th;
+  Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
+    (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
 
 (*Rewrite the subgoal of a proof state (represented by a theorem)*)
 fun rewrite_goal_rule mode prover ss i thm =
   if 0 < i andalso i <= Thm.nprems_of thm
-  then Conv.goal_conv_rule (rewrite_cterm mode prover ss) i thm
+  then Conv.gconv_rule (rewrite_cterm mode prover ss) i thm
   else raise THM ("rewrite_goal_rule", i, [thm]);
 
 
diff -r 00751df1f98c -r 9b5ba76de1c2 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Thu Jul 05 00:06:22 2007 +0200
+++ b/src/Pure/tctical.ML	Thu Jul 05 00:06:23 2007 +0200
@@ -522,7 +522,7 @@
 fun SINGLE tacf = Option.map fst o Seq.pull o tacf
 
 (*Conversions as tactics*)
-fun CONVERSION cv i st = Seq.single (Conv.goal_conv_rule cv i st)
+fun CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st)
   handle THM _ => Seq.empty
     | CTERM _ => Seq.empty
     | TERM _ => Seq.empty