--- 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)