# HG changeset patch
# User wenzelm
# Date 981905660 -3600
# Node ID c1be9f2dff4ce1743b36869393de3f1214d2f918
# Parent  bedfd42db83865a518a16478a28e79d0e9e72e69
more robust selection of calculational rules;

diff -r bedfd42db838 -r c1be9f2dff4c NEWS
--- a/NEWS	Sun Feb 11 16:31:54 2001 +0100
+++ b/NEWS	Sun Feb 11 16:34:20 2001 +0100
@@ -90,6 +90,8 @@
 * Pure: ?thesis / ?this / "..." now work for pure meta-level
 statements as well;
 
+* Pure: more robust selection of calculational rules;
+
 * Pure: the builtin notion of 'finished' goal now includes the ==-refl
 rule (as well as the assumption rule);
 
diff -r bedfd42db838 -r c1be9f2dff4c src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Sun Feb 11 16:31:54 2001 +0100
+++ b/src/Pure/Isar/calculation.ML	Sun Feb 11 16:34:20 2001 +0100
@@ -123,26 +123,23 @@
 
 fun calculate final opt_rules print state =
   let
-    val facts = Proof.the_facts (Proof.assert_forward state);
-
     val strip_assums_concl = Logic.strip_assums_concl o #prop o Thm.rep_thm;
     val eq_prop = op aconv o pairself (Pattern.eta_contract o strip_assums_concl);
-    fun differ thms thms' = not (Library.equal_lists eq_prop (thms, thms'));
+    fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
 
-    fun combine thms =
-      let
-        val ths = thms @ facts;
-        val rs = get_local_rules state;
-        val rules =
-          (case ths of [] => NetRules.rules rs
-          | th :: _ => NetRules.may_unify rs (strip_assums_concl th));
-        val ruleq = Seq.of_list (if_none opt_rules [] @ rules);
-      in Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve ths) ruleq)) end;
+    fun combine ths =
+      (case opt_rules of Some rules => rules
+      | None =>
+          (case ths of [] => NetRules.rules (get_local_rules state)
+          | th :: _ => NetRules.may_unify (get_local_rules state) (strip_assums_concl th)))
+      |> Seq.of_list |> Seq.map (Method.multi_resolve ths) |> Seq.flat
+      |> Seq.filter (not o projection ths);
 
+    val facts = Proof.the_facts (Proof.assert_forward state);
     val (initial, calculations) =
       (case get_calculation state of
         None => (true, Seq.single facts)
-      | Some thms => (false, Seq.filter (differ thms) (combine thms)))
+      | Some calc => (false, Seq.map single (combine (calc @ facts))));
   in
     err_if state (initial andalso final) "No calculation yet";
     err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";