# HG changeset patch
# User wenzelm
# Date 1150234907 -7200
# Node ID 6a346150611a1d07e51b61399e2fb6373e422047
# Parent  51ae6677dd5ffa38afde1d505ba976ed97c2c2a0
(un)varify: tuned exceptions;

diff -r 51ae6677dd5f -r 6a346150611a src/Pure/logic.ML
--- a/src/Pure/logic.ML	Tue Jun 13 23:41:44 2006 +0200
+++ b/src/Pure/logic.ML	Tue Jun 13 23:41:47 2006 +0200
@@ -555,7 +555,8 @@
     (fn Free (x, T) => Var ((x, 0), T)
       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
       | t => t)
-  |> Term.map_term_types varifyT;
+  |> Term.map_term_types varifyT
+  handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
 
 fun unvarify tm =
   tm |> Term.map_aterms
@@ -563,7 +564,8 @@
       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
       | Free (x, _) => raise TERM (bad_fixed x, [tm])
       | t => t)
-  |> Term.map_term_types unvarifyT;
+  |> Term.map_term_types unvarifyT
+  handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
 
 val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T);
 val legacy_unvarifyT = Term.map_atyps (fn TVar ((a, 0), S) => TFree (a, S) | T => T);