simplified unlocalize_mixfix;
authorwenzelm
Tue Dec 12 20:49:32 2006 +0100 (2006-12-12)
changeset 218056af1aa7f67d6
parent 21804 515499542d84
child 21806 6086783d4214
simplified unlocalize_mixfix;
src/Pure/Syntax/mixfix.ML
src/Pure/Tools/class_package.ML
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Tue Dec 12 20:49:31 2006 +0100
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Tue Dec 12 20:49:32 2006 +0100
     1.3 @@ -31,7 +31,7 @@
     1.4    val type_name: string -> mixfix -> string
     1.5    val const_name: string -> mixfix -> string
     1.6    val const_mixfix: string -> mixfix -> string * mixfix
     1.7 -  val unlocalize_mixfix: bool -> mixfix -> mixfix
     1.8 +  val unlocalize_mixfix: mixfix -> mixfix
     1.9    val mixfix_args: mixfix -> int
    1.10  end;
    1.11  
    1.12 @@ -139,9 +139,7 @@
    1.13    | map_mixfix _ Structure = Structure
    1.14    | map_mixfix _ _ = raise Fail ("map_mixfix: illegal occurrence of unnamed infix");
    1.15  
    1.16 -fun unlocalize_mixfix loc mx =
    1.17 -  let val mx' = map_mixfix SynExt.unlocalize_mfix mx
    1.18 -  in if mx = mx' andalso loc then NoSyn else mx' end;
    1.19 +val unlocalize_mixfix = map_mixfix SynExt.unlocalize_mfix;
    1.20  
    1.21  fun mixfix_args NoSyn = 0
    1.22    | mixfix_args (Mixfix (sy, _, _)) = SynExt.mfix_args sy
     2.1 --- a/src/Pure/Tools/class_package.ML	Tue Dec 12 20:49:31 2006 +0100
     2.2 +++ b/src/Pure/Tools/class_package.ML	Tue Dec 12 20:49:32 2006 +0100
     2.3 @@ -333,7 +333,7 @@
     2.4              | _ => error ("More than one type variable in type signature of constant " ^ quote c));
     2.5          val consts1 =
     2.6            Locale.parameters_of thy name_locale
     2.7 -          |> map (apsnd (Syntax.unlocalize_mixfix true))
     2.8 +          |> map (apsnd (TheoryTarget.fork_mixfix false true #> fst))
     2.9          val SOME v = fold extract_classvar consts1 NONE;
    2.10          val consts2 = map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) consts1;
    2.11        in (v, chop (length mapp_sup) consts2) end;
    2.12 @@ -604,7 +604,8 @@
    2.13        || class_bodyP >> pair [])
    2.14      -- P.opt_begin
    2.15      >> (fn ((bname, (supclasses, elems)), begin) =>
    2.16 -        Toplevel.begin_local_theory begin (class bname supclasses elems #-> TheoryTarget.begin)));
    2.17 +        Toplevel.begin_local_theory begin
    2.18 +          (class bname supclasses elems #-> TheoryTarget.begin true)));
    2.19  
    2.20  val instanceP =
    2.21    OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((