fixed comment: "(| _ : _ |)" to "OFCLASS(_, _)"
authorwenzelm
Wed, 20 Jul 1994 12:09:48 +0200
changeset 480 d74522d9437f
parent 479 db5a95f2952e
child 481 ac0568345f88
fixed comment: "(| _ : _ |)" to "OFCLASS(_, _)"
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 =