src/FOL/IFOL.thy

 
 subsection {* Syntax and axiomatic basis *}
 
 global
 
-classes "term" < logic
+classes "term"
 defaultsort "term"
 
 typedecl o
 
 judgment

 subsection {* ``Let'' declarations *}
 
 nonterminals letbinds letbind
 
 constdefs
-  Let :: "['a::logic, 'a => 'b] => ('b::logic)"
+  Let :: "['a::{}, 'a => 'b] => ('b::{})"
     "Let(s, f) == f(s)"
 
 syntax
   "_bind"       :: "[pttrn, 'a] => letbind"           ("(2_ =/ _)" 10)
   ""            :: "letbind => letbinds"              ("_")