src/Pure/ROOT.ML

 instantiation of theorems can lead to inconsistent sorting of type vars if
 'a::S is already present and 'a::T is introduced.
 *)
 
 val banner = "Pure Isabelle";
-val version = "Isabelle-94 revision 6: July 96";
+val version = "Isabelle-94 revision 7: November 96";
 
 print_depth 1;
 
 use "library.ML";
 use "symtab.ML";