# HG changeset patch
# User wenzelm
# Date 1165952972 -3600
# Node ID 6af1aa7f67d6e2434c7a6034daddf11aed7e82a3
# Parent  515499542d842ddc5cad1c9f1c734dea1e8f2ed1
simplified unlocalize_mixfix;

diff -r 515499542d84 -r 6af1aa7f67d6 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Tue Dec 12 20:49:31 2006 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Tue Dec 12 20:49:32 2006 +0100
@@ -31,7 +31,7 @@
   val type_name: string -> mixfix -> string
   val const_name: string -> mixfix -> string
   val const_mixfix: string -> mixfix -> string * mixfix
-  val unlocalize_mixfix: bool -> mixfix -> mixfix
+  val unlocalize_mixfix: mixfix -> mixfix
   val mixfix_args: mixfix -> int
 end;
 
@@ -139,9 +139,7 @@
   | map_mixfix _ Structure = Structure
   | map_mixfix _ _ = raise Fail ("map_mixfix: illegal occurrence of unnamed infix");
 
-fun unlocalize_mixfix loc mx =
-  let val mx' = map_mixfix SynExt.unlocalize_mfix mx
-  in if mx = mx' andalso loc then NoSyn else mx' end;
+val unlocalize_mixfix = map_mixfix SynExt.unlocalize_mfix;
 
 fun mixfix_args NoSyn = 0
   | mixfix_args (Mixfix (sy, _, _)) = SynExt.mfix_args sy
diff -r 515499542d84 -r 6af1aa7f67d6 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Tue Dec 12 20:49:31 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Tue Dec 12 20:49:32 2006 +0100
@@ -333,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 (Syntax.unlocalize_mixfix true))
+          |> map (apsnd (TheoryTarget.fork_mixfix false true #> fst))
         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;
@@ -604,7 +604,8 @@
       || class_bodyP >> pair [])
     -- P.opt_begin
     >> (fn ((bname, (supclasses, elems)), begin) =>
-        Toplevel.begin_local_theory begin (class bname supclasses elems #-> TheoryTarget.begin)));
+        Toplevel.begin_local_theory begin
+          (class bname supclasses elems #-> TheoryTarget.begin true)));
 
 val instanceP =
   OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((