# HG changeset patch
# User haftmann
# Date 1284976536 -7200
# Node ID 9d75d65a1a7ab0f9e7e31a1941e517d833151813
# Parent  92a6ec7464e4425e963a95cda5010aa6c8928b10# Parent  d154f988c247305a5fb8fcd3ef4306dc19aa10ae
merged

diff -r 92a6ec7464e4 -r 9d75d65a1a7a src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Sep 20 11:51:46 2010 +0200
+++ b/src/Pure/Isar/code.ML	Mon Sep 20 11:55:36 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 => ();