src/Pure/Tools/class_package.ML

                 | NONE => SOME v)
             | [] => error ("No type variable in type signature of constant " ^ quote c)
             | _ => 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;
     fun add_consts v raw_cs_sup raw_cs_this thy =
       let

       class_subP --| P.$$$ "+" -- class_bodyP
       || class_subP >> rpair []
       || 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 ((
       P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> wrap_add_instance_sort
       || P.opt_thm_name ":" -- (P.and_list1 parse_arity -- Scan.repeat (P.opt_thm_name ":" -- P.prop))