# HG changeset patch
# User wenzelm
# Date 934230068 -7200
# Node ID 3ddf4a55d765ae43bec59fcd75285b6a740c03d6
# Parent  c8d1002060e89372228960cfa507e8613aba7304
append user rules;

diff -r c8d1002060e8 -r 3ddf4a55d765 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Mon Aug 09 20:53:06 1999 +0200
+++ b/src/Pure/Isar/calculation.ML	Mon Aug 09 22:21:08 1999 +0200
@@ -122,7 +122,7 @@
   let
     fun err_if b msg = if b then raise Proof.STATE (msg, state) else ();
     val fact = Proof.the_fact state;
-    val rules = Seq.of_list (case opt_rules of None => get_local_rules state | Some thms => thms);
+    val rules = Seq.of_list (if_none opt_rules [] @ get_local_rules state);
     val (initial, calculations) =
       (case get_calculation state of
         None => (true, Seq.single fact)