src/Pure/axclass.ML
changeset 28965 1de908189869
parent 28110 9d121b171a0a
child 29524 941ad06c7f9c
     1.1 --- a/src/Pure/axclass.ML	Wed Dec 03 21:00:39 2008 -0800
     1.2 +++ b/src/Pure/axclass.ML	Thu Dec 04 14:43:33 2008 +0100
     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 -    ((Name.binding * attribute list) * term list) list -> theory -> class * theory
     1.8 +    ((Binding.T * 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 @@ -370,7 +370,7 @@
    1.13      thy
    1.14      |> Sign.sticky_prefix name_inst
    1.15      |> Sign.no_base_names
    1.16 -    |> Sign.declare_const [] ((Name.binding c', T'), NoSyn)
    1.17 +    |> Sign.declare_const [] ((Binding.name c', T'), NoSyn)
    1.18      |-> (fn const' as Const (c'', _) => Thm.add_def false true
    1.19            (Thm.def_name c', Logic.mk_equals (Const (c, T'), const'))
    1.20      #>> Thm.varifyT
    1.21 @@ -422,7 +422,7 @@
    1.22      (* class *)
    1.23  
    1.24      val bconst = Logic.const_of_class bclass;
    1.25 -    val class = Sign.full_name thy bclass;
    1.26 +    val class = Sign.full_bname thy bclass;
    1.27      val super = Sign.minimize_sort thy (Sign.certify_sort thy raw_super);
    1.28  
    1.29      fun check_constraint (a, S) =
    1.30 @@ -482,9 +482,9 @@
    1.31        |> Sign.add_path bconst
    1.32        |> Sign.no_base_names
    1.33        |> PureThy.note_thmss ""
    1.34 -        [((Name.binding introN, []), [([Drule.standard raw_intro], [])]),
    1.35 -         ((Name.binding superN, []), [(map Drule.standard raw_classrel, [])]),
    1.36 -         ((Name.binding axiomsN, []),
    1.37 +        [((Binding.name introN, []), [([Drule.standard raw_intro], [])]),
    1.38 +         ((Binding.name superN, []), [(map Drule.standard raw_classrel, [])]),
    1.39 +         ((Binding.name axiomsN, []),
    1.40             [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]
    1.41        ||> Sign.restore_naming def_thy;
    1.42  
    1.43 @@ -530,7 +530,7 @@
    1.44  
    1.45  fun ax_class prep_class prep_classrel (bclass, raw_super) thy =
    1.46    let
    1.47 -    val class = Sign.full_name thy bclass;
    1.48 +    val class = Sign.full_bname thy bclass;
    1.49      val super = map (prep_class thy) raw_super |> Sign.minimize_sort thy;
    1.50    in
    1.51      thy