1.1 --- a/src/Pure/Isar/class_target.ML	Sun Oct 25 20:54:21 2009 +0100
     1.2 +++ b/src/Pure/Isar/class_target.ML	Sun Oct 25 21:35:46 2009 +0100
     1.3 @@ -21,10 +21,8 @@
     1.4  
     1.5    val begin: class list -> sort -> Proof.context -> Proof.context
     1.6    val init: class -> theory -> Proof.context
     1.7 -  val declare: class -> Properties.T
     1.8 -    -> (binding * mixfix) * term -> theory -> theory
     1.9 -  val abbrev: class -> Syntax.mode -> Properties.T
    1.10 -    -> (binding * mixfix) * term -> theory -> theory
    1.11 +  val declare: class -> (binding * mixfix) * term -> theory -> theory
    1.12 +  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory
    1.13    val class_prefix: string -> string
    1.14    val refresh_syntax: class -> Proof.context -> Proof.context
    1.15    val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
    1.16 @@ -325,7 +323,7 @@
    1.17  
    1.18  val class_prefix = Logic.const_of_class o Long_Name.base_name;
    1.19  
    1.20 -fun declare class pos ((c, mx), dict) thy =
    1.21 +fun declare class ((c, mx), dict) thy =
    1.22    let
    1.23      val morph = morphism thy class;
    1.24      val b = Morphism.binding morph c;
    1.25 @@ -337,7 +335,7 @@
    1.26        |> map_types Type.strip_sorts;
    1.27    in
    1.28      thy
    1.29 -    |> Sign.declare_const pos ((b, Type.strip_sorts ty'), mx)
    1.30 +    |> Sign.declare_const ((b, Type.strip_sorts ty'), mx)
    1.31      |> snd
    1.32      |> Thm.add_def false false (b_def, def_eq)
    1.33      |>> Thm.varifyT
    1.34 @@ -347,7 +345,7 @@
    1.35      |> Sign.add_const_constraint (c', SOME ty')
    1.36    end;
    1.37  
    1.38 -fun abbrev class prmode pos ((c, mx), rhs) thy =
    1.39 +fun abbrev class prmode ((c, mx), rhs) thy =
    1.40    let
    1.41      val morph = morphism thy class;
    1.42      val unchecks = these_unchecks thy [class];
    1.43 @@ -358,7 +356,7 @@
    1.44      val rhs'' = map_types Logic.varifyT rhs';
    1.45    in
    1.46      thy
    1.47 -    |> Sign.add_abbrev (#1 prmode) pos (b, rhs'')
    1.48 +    |> Sign.add_abbrev (#1 prmode) (b, rhs'')
    1.49      |> snd
    1.50      |> Sign.add_const_constraint (c', SOME ty')
    1.51      |> Sign.notation true prmode [(Const (c', ty'), mx)]