non-exported syntax
authorhaftmann
Fri, 01 Dec 2006 17:22:33 +0100
changeset 21623 17098171d46a
parent 21622 5825a59785f4
child 21624 6f79647cf536
non-exported syntax
src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Fri Dec 01 17:22:32 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Fri Dec 01 17:22:33 2006 +0100
@@ -322,6 +322,10 @@
     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 =
@@ -333,7 +337,7 @@
             | _ => error ("More than one type variable in type signature of constant " ^ quote c));
         val consts1 =
           Locale.parameters_of thy name_locale
-          |> map (apsnd (Syntax.unlocalize_mixfix true))
+          |> map (apsnd unlocalize)
         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;