src/Pure/Isar/calculation.ML
changeset 15973 5fd94d84470f
parent 15801 d2f5ca3c048d
child 16424 18a07ad8fea8
     1.1 --- a/src/Pure/Isar/calculation.ML	Tue May 17 10:19:43 2005 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Tue May 17 10:19:44 2005 +0200
     1.3 @@ -189,7 +189,7 @@
     1.4        | SOME calc => (false, Seq.map single (combine (calc @ facts))));
     1.5    in
     1.6      err_if state (initial andalso final) "No calculation yet";
     1.7 -    err_if state (initial andalso isSome opt_rules) "Initial calculation -- no rules to be given";
     1.8 +    err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
     1.9      calculations |> Seq.map (fn calc => (print (Proof.context_of state) calc;
    1.10          state |> maintain_calculation final calc))
    1.11    end;