src/Pure/Isar/calculation.ML
changeset 7197 3ddf4a55d765
parent 6903 682f8a9ec75d
child 7414 9bc7797d1249
--- 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)