--- a/src/Pure/Tools/class_package.ML Thu May 10 22:11:37 2007 +0200
+++ b/src/Pure/Tools/class_package.ML Thu May 10 22:11:38 2007 +0200
@@ -33,6 +33,7 @@
val class_of_locale: theory -> string -> class option
val add_def_in_class: local_theory -> string
-> (string * Syntax.mixfix) * ((string * Attrib.src list) * (term * thm)) -> theory -> theory
+ val CLASS_TARGET: bool ref
val print_classes: theory -> unit
val intro_classes_tac: thm list -> tactic
@@ -97,7 +98,8 @@
val superclasses = map (Sign.certify_class thy) raw_superclasses;
val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts;
fun add_const ((c, ty), syn) =
- Sign.add_consts_authentic [(c, ty, syn)] #> pair (Sign.full_name thy c, ty);
+ Sign.add_consts_authentic [(c, ty, syn)]
+ #> pair (Sign.full_name thy c, ty);
fun mk_axioms cs thy =
raw_dep_axioms thy cs
|> (map o apsnd o map) (Sign.cert_prop thy)
@@ -106,7 +108,9 @@
Sign.add_const_constraint_i (c, SOME (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
in
thy
+ (* |> Theory.add_path name *)
|> fold_map add_const consts
+ (* ||> Theory.restore_naming thy *)
|-> (fn cs => mk_axioms cs
#-> (fn axioms_prop => AxClass.define_class (name, superclasses) (map fst cs @ other_consts) axioms_prop
#-> (fn class => `(fn thy => AxClass.get_definition thy class)
@@ -625,6 +629,8 @@
in term :: tfrees @ tvars end;
in (map warning (print_term t); map warning (print_term prop)) end;
+val CLASS_TARGET = ref true;
+
fun add_def_in_class lthy class ((c, syn), ((name, atts), (rhs, eq))) thy =
let
val prfx = (Logic.const_of_class o NameSpace.base) class;