# HG changeset patch
# User wenzelm
# Date 1165761054 -3600
# Node ID 39b2ce38ac66fa208a00340d6a316ab5b545b8f9
# Parent  41986849fee0caa578e6de05fe9685980bf80e0a
interpretation: use C_class name prefix;

diff -r 41986849fee0 -r 39b2ce38ac66 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Sun Dec 10 15:30:53 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Sun Dec 10 15:30:54 2006 +0100
@@ -322,10 +322,6 @@
     val mapp_sup = AList.make
       (the o AList.lookup (op =) ((flat o map (the_parm_map thy) o the_ancestry thy) supclasses))
       ((map (fst o fst) o Locale.parameters_of_expr thy) expr_supclasses);
-    fun unlocalize syn =
-      let
-        val syn' = Syntax.unlocalize_mixfix true syn;
-      in if syn = syn' then NoSyn else syn' end;
     fun extract_tyvar_consts thy name_locale =
       let
         fun extract_classvar ((c, ty), _) w =
@@ -337,7 +333,7 @@
             | _ => error ("More than one type variable in type signature of constant " ^ quote c));
         val consts1 =
           Locale.parameters_of thy name_locale
-          |> map (apsnd unlocalize)
+          |> map (apsnd (Syntax.unlocalize_mixfix true))
         val SOME v = fold extract_classvar consts1 NONE;
         val consts2 = map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) consts1;
       in (v, chop (length mapp_sup) consts2) end;
@@ -381,7 +377,7 @@
           fold (add_global_constraint v name_axclass) mapp_this
     #> add_class_data (name_locale, (name_locale, name_axclass, v, mapp_this,
           map (fst o fst) loc_axioms))
-    #> prove_interpretation_i (bname, [])
+    #> prove_interpretation_i (Logic.const_of_class bname, [])
           (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass v) (map snd (mapp_sup @ mapp_this)))
           ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
     ))))) #> pair name_locale)
@@ -545,7 +541,7 @@
     fun get_thms thy =
       the_ancestry thy sort
       |> AList.make (the_propnames thy)
-      |> map (apsnd (map (NameSpace.append (loc_name))))
+      |> map (apsnd (map (NameSpace.append (Logic.const_of_class loc_name))))
       |> map_filter (fn (superclass, thm_names) =>
           case map_filter (try (PureThy.get_thm thy o Name)) thm_names
            of [] => NONE