src/Pure/Isar/class.ML
changeset 30344 10a67c5ddddb
parent 30335 b3ef64cadcad
child 30585 6b2ba4666336
     1.1 --- a/src/Pure/Isar/class.ML	Sat Mar 07 22:12:07 2009 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Sat Mar 07 22:16:50 2009 +0100
     1.3 @@ -10,9 +10,9 @@
     1.4      (*FIXME the split into class_target.ML, theory_target.ML and
     1.5        class.ML is artificial*)
     1.6  
     1.7 -  val class: bstring -> class list -> Element.context_i list
     1.8 +  val class: binding -> class list -> Element.context_i list
     1.9      -> theory -> string * local_theory
    1.10 -  val class_cmd: bstring -> xstring list -> Element.context list
    1.11 +  val class_cmd: binding -> xstring list -> Element.context list
    1.12      -> theory -> string * local_theory
    1.13    val prove_subclass: tactic -> class -> local_theory -> local_theory
    1.14    val subclass: class -> local_theory -> Proof.state
    1.15 @@ -73,7 +73,7 @@
    1.16      val morph = base_morph $> eq_morph;
    1.17  
    1.18      (* assm_intro *)
    1.19 -    fun prove_assm_intro thm = 
    1.20 +    fun prove_assm_intro thm =
    1.21        let
    1.22          val ((_, [thm']), _) = Variable.import_thms true [thm] empty_ctxt;
    1.23          val thm'' = Morphism.thm (const_morph $> eq_morph) thm';
    1.24 @@ -169,7 +169,7 @@
    1.25      val _ = case filter_out (is_class thy) sups
    1.26       of [] => ()
    1.27        | no_classes => error ("No (proper) classes: " ^ commas (map quote no_classes));
    1.28 -          val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
    1.29 +    val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
    1.30      val supparam_names = map fst supparams;
    1.31      val _ = if has_duplicates (op =) supparam_names
    1.32        then error ("Duplicate parameter(s) in superclasses: "
    1.33 @@ -200,7 +200,7 @@
    1.34        | check_element e = [()];
    1.35      val _ = map check_element syntax_elems;
    1.36      fun fork_syn (Element.Fixes xs) =
    1.37 -          fold_map (fn (c, ty, syn) => cons (Binding.name_of c, syn) #> pair (c, ty, NoSyn)) xs
    1.38 +          fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
    1.39            #>> Element.Fixes
    1.40        | fork_syn x = pair x;
    1.41      val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
    1.42 @@ -217,7 +217,7 @@
    1.43  
    1.44  (* class establishment *)
    1.45  
    1.46 -fun add_consts bname class base_sort sups supparams global_syntax thy =
    1.47 +fun add_consts class base_sort sups supparams global_syntax thy =
    1.48    let
    1.49      (*FIXME simplify*)
    1.50      val supconsts = supparams
    1.51 @@ -227,17 +227,16 @@
    1.52      val raw_params = (snd o chop (length supparams)) all_params;
    1.53      fun add_const (b, SOME raw_ty, _) thy =
    1.54        let
    1.55 -        val v = Binding.name_of b;
    1.56 -        val c = Sign.full_bname thy v;
    1.57 +        val c = Sign.full_name thy b;
    1.58          val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
    1.59          val ty0 = Type.strip_sorts ty;
    1.60          val ty' = map_atyps (K (TFree (Name.aT, [class]))) ty0;
    1.61 -        val syn = (the_default NoSyn o AList.lookup (op =) global_syntax) v;
    1.62 +        val syn = (the_default NoSyn o AList.lookup Binding.eq_name global_syntax) b;
    1.63        in
    1.64          thy
    1.65 -        |> Sign.declare_const [] ((Binding.name v, ty0), syn)
    1.66 +        |> Sign.declare_const [] ((b, ty0), syn)
    1.67          |> snd
    1.68 -        |> pair ((v, ty), (c, ty'))
    1.69 +        |> pair ((Binding.name_of b, ty), (c, ty'))
    1.70        end;
    1.71    in
    1.72      thy
    1.73 @@ -261,7 +260,7 @@
    1.74        | [thm] => SOME thm;
    1.75    in
    1.76      thy
    1.77 -    |> add_consts bname class base_sort sups supparams global_syntax
    1.78 +    |> add_consts class base_sort sups supparams global_syntax
    1.79      |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
    1.80            (map (fst o snd) params)
    1.81            [(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)]
    1.82 @@ -273,12 +272,12 @@
    1.83  
    1.84  fun gen_class prep_spec bname raw_supclasses raw_elems thy =
    1.85    let
    1.86 -    val class = Sign.full_bname thy bname;
    1.87 +    val class = Sign.full_name thy bname;
    1.88      val (((sups, supparams), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
    1.89        prep_spec thy raw_supclasses raw_elems;
    1.90    in
    1.91      thy
    1.92 -    |> Expression.add_locale bname "" supexpr elems
    1.93 +    |> Expression.add_locale bname Binding.empty supexpr elems
    1.94      |> snd |> LocalTheory.exit_global
    1.95      |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
    1.96      |-> (fn (param_map, params, assm_axiom) =>