proper input abbreviations in class
authorhaftmann
Tue Apr 29 15:25:50 2008 +0200 (2008-04-29)
changeset 26761190da765a628
parent 26760 2de4ba348f06
child 26762 78ed28528ca6
proper input abbreviations in class
src/Pure/Isar/class.ML
     1.1 --- a/src/Pure/Isar/class.ML	Tue Apr 29 13:41:11 2008 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Tue Apr 29 15:25:50 2008 +0200
     1.3 @@ -619,7 +619,7 @@
     1.4      |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs'') |> snd
     1.5      |> Sign.add_const_constraint (c', SOME ty')
     1.6      |> Sign.notation true prmode [(Const (c', ty'), mx)]
     1.7 -    |> register_operation class (c', (rhs', NONE))
     1.8 +    |> not (#1 prmode = PrintMode.input) ? register_operation class (c', (rhs', NONE))
     1.9      |> Sign.restore_naming thy
    1.10    end;
    1.11