src/Pure/Isar/calculation.ML

 
 
 
 (** proof commands **)
 
-fun err_if state b msg = if b then raise Proof.STATE (msg, state) else ();
+fun err_if b msg = if b then error msg else ();
 
 fun assert_sane final =
   if final then Proof.assert_forward else Proof.assert_forward_or_chain;
 
 fun maintain_calculation false calc = put_calculation (SOME calc)

     val (initial, calculations) =
       (case get_calculation state of
         NONE => (true, Seq.single facts)
       | SOME calc => (false, Seq.map single (combine (calc @ facts))));
   in
-    err_if state (initial andalso final) "No calculation yet";
-    err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
+    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_calculation int (Proof.context_of state) calc;
         state |> maintain_calculation final calc))
   end;
 
 val also = calculate Proof.get_thmss false;

       (case get_calculation state of
         NONE => (true, [])
       | SOME thms => (false, thms));
     val calc = thms @ facts;
   in
-    err_if state (initial andalso final) "No calculation yet";
+    err_if (initial andalso final) "No calculation yet";
     print_calculation int (Proof.context_of state) calc;
     state |> maintain_calculation final calc
   end;
 
 val moreover = collect false;