# HG changeset patch
# User wenzelm
# Date 774698988 -7200
# Node ID d74522d9437f0b277308f5463348cce2537968f1
# Parent  db5a95f2952e60cc6058d44f6f3cc964383dd398
fixed comment: "(| _ : _ |)" to "OFCLASS(_, _)"

diff -r db5a95f2952e -r d74522d9437f src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Jul 18 12:24:35 1994 +0200
+++ b/src/Pure/thm.ML	Wed Jul 20 12:09:48 1994 +0200
@@ -760,7 +760,7 @@
       else Thm{sign= sign, maxidx= maxidx, hyps= [], prop= implies$A$A}
   end;
 
-(*Axiom-scheme reflecting signature contents: "(| ?'a::c : c_class |)".
+(*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)".
   Is weaker than some definition of c_class, e.g. "c_class == %x.T";
   may be interpreted as an instance of A==>A.*)
 fun class_triv thy c =