append user rules;
authorwenzelm
Mon, 09 Aug 1999 22:21:08 +0200
changeset 7197 3ddf4a55d765
parent 7196 c8d1002060e8
child 7198 680d43e41b0d
append user rules;
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)