(class target)
authorhaftmann
Thu May 10 22:11:38 2007 +0200 (2007-05-10)
changeset 22930f99617e7103f
parent 22929 e6b6f8dd03e9
child 22931 11cc1ccad58e
(class target)
src/Pure/Tools/class_package.ML
     1.1 --- a/src/Pure/Tools/class_package.ML	Thu May 10 22:11:37 2007 +0200
     1.2 +++ b/src/Pure/Tools/class_package.ML	Thu May 10 22:11:38 2007 +0200
     1.3 @@ -33,6 +33,7 @@
     1.4    val class_of_locale: theory -> string -> class option
     1.5    val add_def_in_class: local_theory -> string
     1.6      -> (string * Syntax.mixfix) * ((string * Attrib.src list) * (term * thm)) -> theory -> theory
     1.7 +  val CLASS_TARGET: bool ref
     1.8  
     1.9    val print_classes: theory -> unit
    1.10    val intro_classes_tac: thm list -> tactic
    1.11 @@ -97,7 +98,8 @@
    1.12      val superclasses = map (Sign.certify_class thy) raw_superclasses;
    1.13      val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts;
    1.14      fun add_const ((c, ty), syn) =
    1.15 -      Sign.add_consts_authentic [(c, ty, syn)] #> pair (Sign.full_name thy c, ty);
    1.16 +      Sign.add_consts_authentic [(c, ty, syn)]
    1.17 +      #> pair (Sign.full_name thy c, ty);
    1.18      fun mk_axioms cs thy =
    1.19        raw_dep_axioms thy cs
    1.20        |> (map o apsnd o map) (Sign.cert_prop thy)
    1.21 @@ -106,7 +108,9 @@
    1.22        Sign.add_const_constraint_i (c, SOME (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
    1.23    in
    1.24      thy
    1.25 +    (* |> Theory.add_path name *)
    1.26      |> fold_map add_const consts
    1.27 +    (* ||> Theory.restore_naming thy *)
    1.28      |-> (fn cs => mk_axioms cs
    1.29      #-> (fn axioms_prop => AxClass.define_class (name, superclasses) (map fst cs @ other_consts) axioms_prop
    1.30      #-> (fn class => `(fn thy => AxClass.get_definition thy class)
    1.31 @@ -625,6 +629,8 @@
    1.32        in term :: tfrees @ tvars end;
    1.33    in (map warning (print_term t); map warning (print_term prop)) end;
    1.34  
    1.35 +val CLASS_TARGET = ref true;
    1.36 +
    1.37  fun add_def_in_class lthy class ((c, syn), ((name, atts), (rhs, eq))) thy =
    1.38    let
    1.39      val prfx = (Logic.const_of_class o NameSpace.base) class;