src/Pure/type_infer.ML
changeset 39291 4b632bb847a8
parent 39290 44e4d8dfd6bf
child 39292 6f085332c7d3
     1.1 --- a/src/Pure/type_infer.ML	Sun Sep 12 20:47:47 2010 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Sun Sep 12 21:24:23 2010 +0200
     1.3 @@ -157,7 +157,7 @@
     1.4              SOME U =>
     1.5                let val (pU, idx') = polyT_of U idx
     1.6                in constraint T (PConst (c, pU)) (ps, idx') end
     1.7 -          | NONE => raise TYPE ("Undeclared constant: " ^ quote c, [], []))
     1.8 +          | NONE => error ("Undeclared constant: " ^ quote c))
     1.9        | pre_of (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) =
    1.10            let val (pT, idx') = polyT_of T idx
    1.11            in (PVar (xi, pT), (ps, idx')) end
    1.12 @@ -265,8 +265,7 @@
    1.13            else (Inttab.update_new (i,
    1.14              Param (idx, Sign.inter_sort thy (S', S))) tye, idx + 1)
    1.15        | meet (PType (a, Ts), S) (tye_idx as (tye, _)) =
    1.16 -          meets (Ts, arity_sorts a S
    1.17 -            handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx
    1.18 +          meets (Ts, arity_sorts a S handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx
    1.19        | meet (PTFree (x, S'), S) (tye_idx as (tye, _)) =
    1.20            if Sign.subsort thy (S', S) then tye_idx
    1.21            else raise NO_UNIFIER (not_of_sort x S' S, tye)
    1.22 @@ -336,25 +335,20 @@
    1.23            in Term.subst_bounds (map Syntax.mark_boundT xs, t) end;
    1.24        in (map prep ts', Ts') end;
    1.25  
    1.26 -    fun err_loose i =
    1.27 -      raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], []);
    1.28 +    fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
    1.29  
    1.30      fun unif_failed msg =
    1.31        "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
    1.32  
    1.33      fun err_appl msg tye bs t T u U =
    1.34 -      let
    1.35 -        val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U];
    1.36 -        val text = unif_failed msg ^ Type.appl_error pp t' T' u' U' ^ "\n";
    1.37 -      in raise TYPE (text, [T', U'], [t', u']) end;
    1.38 +      let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U]
    1.39 +      in error (unif_failed msg ^ Type.appl_error pp t' T' u' U' ^ "\n") end;
    1.40  
    1.41      fun err_constraint msg tye bs t T U =
    1.42 -      let
    1.43 -        val ([t'], [T', U']) = prep_output tye bs [t] [T, U];
    1.44 -        val text =
    1.45 -          unif_failed msg ^
    1.46 -            Type.appl_error pp (Const ("_type_constraint_", U' --> U')) (U' --> U') t' T' ^ "\n";
    1.47 -      in raise TYPE (text, [T', U'], [t']) end;
    1.48 +      let val ([t'], [T', U']) = prep_output tye bs [t] [T, U] in
    1.49 +        error (unif_failed msg ^
    1.50 +          Type.appl_error pp (Const ("_type_constraint_", U' --> U')) (U' --> U') t' T' ^ "\n")
    1.51 +      end;
    1.52  
    1.53  
    1.54      (* main *)