src/Pure/axclass.ML
changeset 28083 103d9282a946
parent 28014 fe36718702aa
child 28110 9d121b171a0a
     1.1 --- a/src/Pure/axclass.ML	Tue Sep 02 14:10:32 2008 +0200
     1.2 +++ b/src/Pure/axclass.ML	Tue Sep 02 14:10:45 2008 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  signature AX_CLASS =
     1.5  sig
     1.6    val define_class: bstring * class list -> string list ->
     1.7 -    ((bstring * attribute list) * term list) list -> theory -> class * theory
     1.8 +    ((Name.binding * attribute list) * term list) list -> theory -> class * theory
     1.9    val add_classrel: thm -> theory -> theory
    1.10    val add_arity: thm -> theory -> theory
    1.11    val prove_classrel: class * class -> tactic -> theory -> theory
    1.12 @@ -482,9 +482,10 @@
    1.13        |> Sign.add_path bconst
    1.14        |> Sign.no_base_names
    1.15        |> PureThy.note_thmss ""
    1.16 -        [((introN, []), [([Drule.standard raw_intro], [])]),
    1.17 -         ((superN, []), [(map Drule.standard raw_classrel, [])]),
    1.18 -         ((axiomsN, []), [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]
    1.19 +        [((Name.binding introN, []), [([Drule.standard raw_intro], [])]),
    1.20 +         ((Name.binding superN, []), [(map Drule.standard raw_classrel, [])]),
    1.21 +         ((Name.binding axiomsN, []),
    1.22 +           [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]
    1.23        ||> Sign.restore_naming def_thy;
    1.24  
    1.25