Type_Infer.infer_types: plain error instead of kernel exception TYPE;
authorwenzelm
Sun Sep 12 21:24:23 2010 +0200 (2010-09-12)
changeset 392914b632bb847a8
parent 39290 44e4d8dfd6bf
child 39292 6f085332c7d3
Type_Infer.infer_types: plain error instead of kernel exception TYPE;
src/Pure/Isar/proof_context.ML
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sun Sep 12 20:47:47 2010 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Sep 12 21:24:23 2010 +0200
     1.3 @@ -698,9 +698,8 @@
     1.4    let val Mode {pattern, ...} = get_mode ctxt
     1.5    in Variable.def_type ctxt pattern end;
     1.6  
     1.7 -fun standard_infer_types ctxt ts =
     1.8 -  Type_Infer.infer_types ctxt (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt) ts
     1.9 -  handle TYPE (msg, _, _) => error msg;
    1.10 +fun standard_infer_types ctxt =
    1.11 +  Type_Infer.infer_types ctxt (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt);
    1.12  
    1.13  local
    1.14  
     2.1 --- a/src/Pure/type_infer.ML	Sun Sep 12 20:47:47 2010 +0200
     2.2 +++ b/src/Pure/type_infer.ML	Sun Sep 12 21:24:23 2010 +0200
     2.3 @@ -157,7 +157,7 @@
     2.4              SOME U =>
     2.5                let val (pU, idx') = polyT_of U idx
     2.6                in constraint T (PConst (c, pU)) (ps, idx') end
     2.7 -          | NONE => raise TYPE ("Undeclared constant: " ^ quote c, [], []))
     2.8 +          | NONE => error ("Undeclared constant: " ^ quote c))
     2.9        | pre_of (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) =
    2.10            let val (pT, idx') = polyT_of T idx
    2.11            in (PVar (xi, pT), (ps, idx')) end
    2.12 @@ -265,8 +265,7 @@
    2.13            else (Inttab.update_new (i,
    2.14              Param (idx, Sign.inter_sort thy (S', S))) tye, idx + 1)
    2.15        | meet (PType (a, Ts), S) (tye_idx as (tye, _)) =
    2.16 -          meets (Ts, arity_sorts a S
    2.17 -            handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx
    2.18 +          meets (Ts, arity_sorts a S handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx
    2.19        | meet (PTFree (x, S'), S) (tye_idx as (tye, _)) =
    2.20            if Sign.subsort thy (S', S) then tye_idx
    2.21            else raise NO_UNIFIER (not_of_sort x S' S, tye)
    2.22 @@ -336,25 +335,20 @@
    2.23            in Term.subst_bounds (map Syntax.mark_boundT xs, t) end;
    2.24        in (map prep ts', Ts') end;
    2.25  
    2.26 -    fun err_loose i =
    2.27 -      raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], []);
    2.28 +    fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
    2.29  
    2.30      fun unif_failed msg =
    2.31        "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
    2.32  
    2.33      fun err_appl msg tye bs t T u U =
    2.34 -      let
    2.35 -        val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U];
    2.36 -        val text = unif_failed msg ^ Type.appl_error pp t' T' u' U' ^ "\n";
    2.37 -      in raise TYPE (text, [T', U'], [t', u']) end;
    2.38 +      let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U]
    2.39 +      in error (unif_failed msg ^ Type.appl_error pp t' T' u' U' ^ "\n") end;
    2.40  
    2.41      fun err_constraint msg tye bs t T U =
    2.42 -      let
    2.43 -        val ([t'], [T', U']) = prep_output tye bs [t] [T, U];
    2.44 -        val text =
    2.45 -          unif_failed msg ^
    2.46 -            Type.appl_error pp (Const ("_type_constraint_", U' --> U')) (U' --> U') t' T' ^ "\n";
    2.47 -      in raise TYPE (text, [T', U'], [t']) end;
    2.48 +      let val ([t'], [T', U']) = prep_output tye bs [t] [T, U] in
    2.49 +        error (unif_failed msg ^
    2.50 +          Type.appl_error pp (Const ("_type_constraint_", U' --> U')) (U' --> U') t' T' ^ "\n")
    2.51 +      end;
    2.52  
    2.53  
    2.54      (* main *)