# HG changeset patch
# User haftmann
# Date 1178827898 -7200
# Node ID f99617e7103f3a2fbf4f1d10e9920f634983c6b0
# Parent  e6b6f8dd03e9811639c55589f1a7bb61dabf2491
(class target)

diff -r e6b6f8dd03e9 -r f99617e7103f src/Pure/Tools/class_package.ML
--- 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;