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 4: August 95";
+val version = "Isabelle-94 revision 5: January 96";
 
 print_depth 1;
 
 use "library.ML";
 use "symtab.ML";