src/Pure/Isar/class_target.ML
changeset 37146 f652333bbf8e
parent 37145 01aa36932739
child 37236 739d8b9c59da
     1.1 --- a/src/Pure/Isar/class_target.ML	Thu May 27 17:41:27 2010 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Thu May 27 18:10:37 2010 +0200
     1.3 @@ -355,7 +355,7 @@
     1.4      |> snd
     1.5      |> Sign.add_const_constraint (c', SOME ty')
     1.6      |> Sign.notation true prmode [(Const (c', ty'), mx)]
     1.7 -    |> not (#1 prmode = PrintMode.input) ? register_operation class (c', (rhs', NONE))
     1.8 +    |> not (#1 prmode = Print_Mode.input) ? register_operation class (c', (rhs', NONE))
     1.9    end;
    1.10  
    1.11