# HG changeset patch
# User haftmann
# Date 1248183871 -7200
# Node ID 4ee1c1aebbcc62e9b090ecbdc470af519bdd69c9
# Parent  a7bc3141e599fb44925e87a0a6adac4377903d0b
more accurate check of judgment type

diff -r a7bc3141e599 -r 4ee1c1aebbcc src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Jul 21 15:44:30 2009 +0200
+++ b/src/Pure/Isar/code.ML	Tue Jul 21 15:44:31 2009 +0200
@@ -801,7 +801,9 @@
      of SOME T_class => T_class
       | _ => error ("Bad certificate: " ^ Display.string_of_thm thm);
     val tvar = case try Term.dest_TVar T
-     of SOME tvar => tvar
+     of SOME (tvar as (_, sort)) => if null (filter (can (AxClass.get_info thy)) sort)
+          then tvar
+          else error ("Bad sort: " ^ Display.string_of_thm thm)
       | _ => error ("Bad type: " ^ Display.string_of_thm thm);
     val _ = if Term.add_tvars eqn [] = [tvar] then ()
       else error ("Inconsistent type: " ^ Display.string_of_thm thm);