1.1 --- a/src/Pure/proofterm.ML	Thu May 13 18:22:10 2010 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Thu May 13 18:47:07 2010 +0200
     1.3 @@ -347,7 +347,7 @@
     1.4  fun change_type opTs (PAxm (name, prop, _)) = PAxm (name, prop, opTs)
     1.5    | change_type (SOME [T]) (OfClass (_, c)) = OfClass (T, c)
     1.6    | change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs)
     1.7 -  | change_type opTs (Promise _) = error "change_type: unexpected promise"
     1.8 +  | change_type opTs (Promise _) = raise Fail "change_type: unexpected promise"
     1.9    | change_type opTs (PThm (i, ((name, prop, _), body))) =
    1.10        PThm (i, ((name, prop, opTs), body))
    1.11    | change_type _ prf = prf;
    1.12 @@ -1074,7 +1074,7 @@
    1.13                | Oracle (_, prop, _) => prop
    1.14                | Promise (_, prop, _) => prop
    1.15                | PThm (_, ((_, prop, _), _)) => prop
    1.16 -              | _ => error "shrink: proof not in normal form");
    1.17 +              | _ => raise Fail "shrink: proof not in normal form");
    1.18              val vs = vars_of prop;
    1.19              val (ts', ts'') = chop (length vs) ts;
    1.20              val insts = take (length ts') (map (fst o dest_Var) vs) ~~ ts';
    1.21 @@ -1351,9 +1351,9 @@
    1.22    let
    1.23      val _ = prop |> Term.exists_subterm (fn t =>
    1.24        (Term.is_Free t orelse Term.is_Var t) andalso
    1.25 -        error ("promise_proof: illegal variable " ^ Syntax.string_of_term_global thy t));
    1.26 +        raise Fail ("promise_proof: illegal variable " ^ Syntax.string_of_term_global thy t));
    1.27      val _ = prop |> Term.exists_type (Term.exists_subtype
    1.28 -      (fn TFree (a, _) => error ("promise_proof: illegal type variable " ^ quote a)
    1.29 +      (fn TFree (a, _) => raise Fail ("promise_proof: illegal type variable " ^ quote a)
    1.30          | _ => false));
    1.31    in Promise (i, prop, map TVar (Term.add_tvars prop [])) end;
    1.32