changeset 26761 | 190da765a628 |
parent 26730 | bbb5e6904d78 |
child 26939 | 1035c89b4c02 |
--- 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;