# HG changeset patch # User haftmann # Date 1267017594 -3600 # Node ID 997a23ae1aa053ad572917e83d5e760e4faba2e9 # Parent e4a7947e02b8669c47c01748d0c64be421a714dd more precise exception handler diff -r e4a7947e02b8 -r 997a23ae1aa0 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Wed Feb 24 14:19:53 2010 +0100 +++ b/src/Pure/Isar/code.ML Wed Feb 24 14:19:54 2010 +0100 @@ -420,7 +420,7 @@ of Type ("fun", [ty, ty_abs]) => (ty, ty_abs) | _ => error ("Not a datatype abstractor:\n" ^ string_of_const thy abs ^ " :: " ^ string_of_typ thy ty'); - val _ = Thm.cterm_of thy (Const (rep, ty_abs --> ty)) handle CTERM _ => + val _ = Thm.cterm_of thy (Const (rep, ty_abs --> ty)) handle TYPE _ => error ("Not a projection:\n" ^ string_of_const thy rep); val cert = Logic.mk_equals (Const (abs, ty --> ty_abs) $ (Const (rep, ty_abs --> ty) $ Free ("x", ty_abs)), Free ("x", ty_abs));