src/Pure/logic.ML
changeset 19879 6a346150611a
parent 19806 f860b7a98445
child 20078 f4122d7494f3
     1.1 --- a/src/Pure/logic.ML	Tue Jun 13 23:41:44 2006 +0200
     1.2 +++ b/src/Pure/logic.ML	Tue Jun 13 23:41:47 2006 +0200
     1.3 @@ -555,7 +555,8 @@
     1.4      (fn Free (x, T) => Var ((x, 0), T)
     1.5        | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
     1.6        | t => t)
     1.7 -  |> Term.map_term_types varifyT;
     1.8 +  |> Term.map_term_types varifyT
     1.9 +  handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
    1.10  
    1.11  fun unvarify tm =
    1.12    tm |> Term.map_aterms
    1.13 @@ -563,7 +564,8 @@
    1.14        | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
    1.15        | Free (x, _) => raise TERM (bad_fixed x, [tm])
    1.16        | t => t)
    1.17 -  |> Term.map_term_types unvarifyT;
    1.18 +  |> Term.map_term_types unvarifyT
    1.19 +  handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
    1.20  
    1.21  val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T);
    1.22  val legacy_unvarifyT = Term.map_atyps (fn TVar ((a, 0), S) => TFree (a, S) | T => T);