src/Pure/Isar/class.ML
changeset 26761 190da765a628
parent 26730 bbb5e6904d78
child 26939 1035c89b4c02
equal deleted inserted replaced
26760:2de4ba348f06 26761:190da765a628
   617   in
   617   in
   618     thy'
   618     thy'
   619     |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs'') |> snd
   619     |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs'') |> snd
   620     |> Sign.add_const_constraint (c', SOME ty')
   620     |> Sign.add_const_constraint (c', SOME ty')
   621     |> Sign.notation true prmode [(Const (c', ty'), mx)]
   621     |> Sign.notation true prmode [(Const (c', ty'), mx)]
   622     |> register_operation class (c', (rhs', NONE))
   622     |> not (#1 prmode = PrintMode.input) ? register_operation class (c', (rhs', NONE))
   623     |> Sign.restore_naming thy
   623     |> Sign.restore_naming thy
   624   end;
   624   end;
   625 
   625 
   626 
   626 
   627 (** instantiation target **)
   627 (** instantiation target **)