# HG changeset patch
# User wenzelm
# Date 954612710 -7200
# Node ID dc496bb0638f7c1dff4cbcb0463853c54f4eb417
# Parent  7461dc59a818e6e60d6e2424443588bb504403d8
more robust handling of explicit rules;

diff -r 7461dc59a818 -r dc496bb0638f src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Sat Apr 01 20:10:57 2000 +0200
+++ b/src/Pure/Isar/calculation.ML	Sat Apr 01 20:11:50 2000 +0200
@@ -130,11 +130,11 @@
     fun combine thms =
       let
         val ths = thms @ facts;
-        val rs = NetRules.inserts (if_none opt_rules []) (get_local_rules state);
+        val rs = get_local_rules state;
         val rules =
           (case ths of [] => NetRules.rules rs
           | th :: _ => NetRules.may_unify rs (Logic.strip_assums_concl (#prop (Thm.rep_thm th))));
-        val ruleq = Seq.of_list rules;
+        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;
 
     val (initial, calculations) =