# HG changeset patch # User haftmann # Date 1164990153 -3600 # Node ID 17098171d46aefc6f1c2cf19c2c2c5c8ce99aa34 # Parent 5825a59785f4d3d2e0c9fc9a4747340a3e70e6aa non-exported syntax diff -r 5825a59785f4 -r 17098171d46a 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;