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 3: April 95";
+val version = "Isabelle-94 revision 4: August 95";
 
 print_depth 1;
 
 use "library.ML";
 use "term.ML";