# HG changeset patch
# User wenzelm
# Date 931287963 -7200
# Node ID 682f8a9ec75d40e5dfe60cc886c20fbd7a7578d1
# Parent  5f126c4957712d678cd33555278a09341f7c6514
improved errors;

diff -r 5f126c495771 -r 682f8a9ec75d src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Tue Jul 06 21:04:37 1999 +0200
+++ b/src/Pure/Isar/calculation.ML	Tue Jul 06 21:06:03 1999 +0200
@@ -120,13 +120,16 @@
 
 fun calculate final opt_rules print state =
   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 calculations =
+    val (initial, calculations) =
       (case get_calculation state of
-        None => Seq.single fact
-      | Some thm => Seq.flat (Seq.map (Method.multi_resolve [thm, fact]) rules));
+        None => (true, Seq.single fact)
+      | Some thm => (false, Seq.flat (Seq.map (Method.multi_resolve [thm, fact]) rules)));
   in
+    err_if (initial andalso final) "No calculation yet";
+    err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
     calculations |> Seq.map (fn calc =>
       (print calc;
         (if final then