src/Pure/Isar/class.ML
changeset 36635 080b755377c0
parent 36464 b789c1731fb7
child 36645 30bd207ec222
     1.1 --- a/src/Pure/Isar/class.ML	Tue May 04 08:55:39 2010 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Tue May 04 08:55:43 2010 +0200
     1.3 @@ -276,16 +276,16 @@
     1.4      #> pair (param_map, params, assm_axiom)))
     1.5    end;
     1.6  
     1.7 -fun gen_class prep_class_spec bname raw_supclasses raw_elems thy =
     1.8 +fun gen_class prep_class_spec b raw_supclasses raw_elems thy =
     1.9    let
    1.10 -    val class = Sign.full_name thy bname;
    1.11 +    val class = Sign.full_name thy b;
    1.12      val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
    1.13        prep_class_spec thy raw_supclasses raw_elems;
    1.14    in
    1.15      thy
    1.16 -    |> Expression.add_locale bname Binding.empty supexpr elems
    1.17 +    |> Expression.add_locale b (Binding.qualify true "class" b) supexpr elems
    1.18      |> snd |> Local_Theory.exit_global
    1.19 -    |> adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax
    1.20 +    |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
    1.21      ||> Theory.checkpoint
    1.22      |-> (fn (param_map, params, assm_axiom) =>
    1.23         `(fn thy => calculate thy class sups base_sort param_map assm_axiom)