diff -r 49c319fff40c -r d154f988c247 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Sep 20 09:19:22 2010 +0200
+++ b/src/Pure/Isar/code.ML	Mon Sep 20 11:55:21 2010 +0200
@@ -543,7 +543,8 @@
       handle TERM _ => bad "Not an abstract equation";
     val (rep_const, ty) = dest_Const rep;
     val (tyco, sorts) = ((apsnd o map) (snd o dest_TVar) o dest_Type o domain_type) ty
-      handle TERM _ => bad "Not an abstract equation";
+      handle TERM _ => bad "Not an abstract equation"
+           | TYPE _ => bad "Not an abstract equation";
     val _ = case some_tyco of SOME tyco' => if tyco = tyco' then ()
           else bad ("Abstract type mismatch:" ^ quote tyco ^ " vs. " ^ quote tyco')
       | NONE => ();