diff -r 2de4ba348f06 -r 190da765a628 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue Apr 29 13:41:11 2008 +0200
+++ b/src/Pure/Isar/class.ML	Tue Apr 29 15:25:50 2008 +0200
@@ -619,7 +619,7 @@
     |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs'') |> snd
     |> Sign.add_const_constraint (c', SOME ty')
     |> Sign.notation true prmode [(Const (c', ty'), mx)]
-    |> register_operation class (c', (rhs', NONE))
+    |> not (#1 prmode = PrintMode.input) ? register_operation class (c', (rhs', NONE))
     |> Sign.restore_naming thy
   end;