src/Pure/Isar/class.ML
changeset 28084 a05ca48ef263
parent 28083 103d9282a946
child 28085 914183e229e9
     1.1 --- a/src/Pure/Isar/class.ML	Tue Sep 02 14:10:45 2008 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Tue Sep 02 16:55:33 2008 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4    val abbrev: class -> Syntax.mode -> Properties.T
     1.5      -> (string * mixfix) * term -> theory -> theory
     1.6    val note: class -> string
     1.7 -    -> ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list
     1.8 +    -> (Attrib.binding * (thm list * Attrib.src list) list) list
     1.9      -> theory -> (bstring * thm list) list * theory
    1.10    val declaration: class -> declaration -> theory -> theory
    1.11    val refresh_syntax: class -> Proof.context -> Proof.context
    1.12 @@ -48,7 +48,7 @@
    1.13  
    1.14    (*old axclass layer*)
    1.15    val axclass_cmd: bstring * xstring list
    1.16 -    -> ((Name.binding * Attrib.src list) * string list) list
    1.17 +    -> (Attrib.binding * string list) list
    1.18      -> theory -> class * theory
    1.19    val classrel_cmd: xstring * xstring -> theory -> Proof.state
    1.20  
    1.21 @@ -374,7 +374,7 @@
    1.22      thy
    1.23      |> fold2 add_constraint (map snd consts) no_constraints
    1.24      |> prove_interpretation tac ((false, prfx), []) (Locale.Locale class)
    1.25 -          (inst, map (fn def => ((Name.no_binding, []), def)) defs)
    1.26 +          (inst, map (fn def => (Attrib.no_binding, def)) defs)
    1.27      |> fold2 add_constraint (map snd consts) constraints
    1.28    end;
    1.29