--- 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
--- 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]);
--- 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