# HG changeset patch
# User wenzelm
# Date 978900116 -3600
# Node ID dcb75538f542795e7ecdb8a1fec4938a93be24cf
# Parent  2ddfc42b7f51e29264efa8be7b15e9f2b21cea6f
CHANGED_PROP;

diff -r 2ddfc42b7f51 -r dcb75538f542 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Sun Jan 07 21:40:49 2001 +0100
+++ b/src/HOL/Tools/meson.ML	Sun Jan 07 21:41:56 2001 +0100
@@ -383,7 +383,8 @@
 local
 
 fun meson_meth ctxt =
-  Method.SIMPLE_METHOD' HEADGOAL (CHANGED o meson_claset_tac (Classical.get_local_claset ctxt));
+  Method.SIMPLE_METHOD' HEADGOAL
+    (CHANGED_PROP o meson_claset_tac (Classical.get_local_claset ctxt));
 
 in
 
diff -r 2ddfc42b7f51 -r dcb75538f542 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Sun Jan 07 21:40:49 2001 +0100
+++ b/src/Provers/clasimp.ML	Sun Jan 07 21:41:56 2001 +0100
@@ -315,8 +315,8 @@
 fun auto_args m =
   Method.bang_sectioned_args' clasimp_modifiers (Scan.lift (Scan.option (Args.nat -- Args.nat))) m;
 
-fun auto_meth None = clasimp_meth (CHANGED o auto_tac)
-  | auto_meth (Some (m, n)) = clasimp_meth (CHANGED o (fn css => mk_auto_tac css m n));
+fun auto_meth None = clasimp_meth (CHANGED_PROP o auto_tac)
+  | auto_meth (Some (m, n)) = clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n));
 
 
 (* theory setup *)
@@ -330,6 +330,6 @@
     ("bestsimp", clasimp_method' best_simp_tac, "combined best and simp"),
     ("force", clasimp_method' force_tac, "force"),
     ("auto", auto_args auto_meth, "auto"),
-    ("clarsimp", clasimp_method' (CHANGED oo clarsimp_tac), "clarify simplified goal")]];
+    ("clarsimp", clasimp_method' (CHANGED_PROP oo clarsimp_tac), "clarify simplified goal")]];
 
 end;
diff -r 2ddfc42b7f51 -r dcb75538f542 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sun Jan 07 21:40:49 2001 +0100
+++ b/src/Provers/classical.ML	Sun Jan 07 21:41:56 2001 +0100
@@ -1192,11 +1192,11 @@
   ("contradiction", Method.no_args contradiction, "proof by contradiction"),
   ("intro", Method.thms_ctxt_args intro, "repeatedly apply introduction rules"),
   ("elim", Method.thms_ctxt_args elim, "repeatedly apply elimination rules"),
-  ("clarify", cla_method' (CHANGED oo clarify_tac), "repeatedly apply safe steps"),
+  ("clarify", cla_method' (CHANGED_PROP oo clarify_tac), "repeatedly apply safe steps"),
   ("fast", cla_method' fast_tac, "classical prover (depth-first)"),
   ("slow", cla_method' slow_tac, "classical prover (slow depth-first)"),
   ("best", cla_method' best_tac, "classical prover (best-first)"),
-  ("safe", cla_method safe_tac, "classical prover (apply safe rules)")];
+  ("safe", cla_method (CHANGED_PROP o safe_tac), "classical prover (apply safe rules)")];
 
 
 
diff -r 2ddfc42b7f51 -r dcb75538f542 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Sun Jan 07 21:40:49 2001 +0100
+++ b/src/Provers/hypsubst.ML	Sun Jan 07 21:41:56 2001 +0100
@@ -257,7 +257,8 @@
 (* proof methods *)
 
 val subst_meth = Method.thm_args (Method.SIMPLE_METHOD' HEADGOAL o stac);
-val hyp_subst_meth = Method.no_args (Method.SIMPLE_METHOD' HEADGOAL hyp_subst_tac);
+val hyp_subst_meth =
+  Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o hyp_subst_tac));
 
 
 (* attributes *)
diff -r 2ddfc42b7f51 -r dcb75538f542 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Sun Jan 07 21:40:49 2001 +0100
+++ b/src/Provers/simplifier.ML	Sun Jan 07 21:41:56 2001 +0100
@@ -542,10 +542,11 @@
 
 fun simp_method (prems, tac) ctxt = Method.METHOD (fn facts =>
   ALLGOALS (Method.insert_tac (prems @ facts)) THEN
-    (CHANGED o ALLGOALS o tac) (get_local_simpset ctxt));
+    (CHANGED_PROP o ALLGOALS o tac) (get_local_simpset ctxt));
 
 fun simp_method' (prems, tac) ctxt = Method.METHOD (fn facts =>
-  HEADGOAL (Method.insert_tac (prems @ facts) THEN' (CHANGED oo tac) (get_local_simpset ctxt)));
+  HEADGOAL (Method.insert_tac (prems @ facts) THEN'
+      (CHANGED_PROP oo tac) (get_local_simpset ctxt)));
 
 
 (* setup_methods *)
diff -r 2ddfc42b7f51 -r dcb75538f542 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Sun Jan 07 21:40:49 2001 +0100
+++ b/src/Provers/splitter.ML	Sun Jan 07 21:41:56 2001 +0100
@@ -427,7 +427,7 @@
 
 val split_args = #2 oo Method.syntax Attrib.local_thms;
 
-fun split_meth ths = Method.SIMPLE_METHOD' HEADGOAL (gen_split_tac ths);
+fun split_meth ths = Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o gen_split_tac ths);
 
 
 
diff -r 2ddfc42b7f51 -r dcb75538f542 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sun Jan 07 21:40:49 2001 +0100
+++ b/src/Pure/Isar/method.ML	Sun Jan 07 21:41:56 2001 +0100
@@ -267,8 +267,8 @@
 
 (* unfold / fold definitions *)
 
-fun unfold thms = SIMPLE_METHOD (CHANGED (rewrite_goals_tac thms));
-fun fold thms = SIMPLE_METHOD (CHANGED (fold_goals_tac thms));
+fun unfold thms = SIMPLE_METHOD (CHANGED_PROP (rewrite_goals_tac thms));
+fun fold thms = SIMPLE_METHOD (CHANGED_PROP (fold_goals_tac thms));
 
 
 (* atomize meta-connectives *)
diff -r 2ddfc42b7f51 -r dcb75538f542 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Sun Jan 07 21:40:49 2001 +0100
+++ b/src/Pure/tctical.ML	Sun Jan 07 21:41:56 2001 +0100
@@ -19,6 +19,7 @@
   val APPEND            : tactic * tactic -> tactic
   val APPEND'           : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
   val CHANGED           : tactic -> tactic
+  val CHANGED_PROP      : tactic -> tactic
   val CHANGED_GOAL	: (int -> tactic) -> int -> tactic
   val COND              : (thm -> bool) -> tactic -> tactic -> tactic   
   val DETERM            : tactic -> tactic
@@ -299,6 +300,12 @@
     let fun diff st' = not (eq_thm(st,st'))
     in  Seq.filter diff (tac st)  end;
 
+fun CHANGED_PROP tac st = 
+    let
+      val prop = #prop (Thm.rep_thm st);
+      fun diff st' = not (prop aconv #prop (Thm.rep_thm st'));
+    in  Seq.filter diff (tac st)  end;
+
 
 (*** Tacticals based on subgoal numbering ***)