# HG changeset patch
# User wenzelm
# Date 1192213316 -7200
# Node ID 8bc74ba1423d46f654bebe4613467829d23881ca
# Parent  61946780de00fae6af31794386d29da68061edc7
fork_mixfix: explicit bool argument;

diff -r 61946780de00 -r 8bc74ba1423d src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Oct 12 18:09:12 2007 +0200
+++ b/src/Pure/Isar/class.ML	Fri Oct 12 20:21:56 2007 +0200
@@ -7,7 +7,7 @@
 
 signature CLASS =
 sig
-  val fork_mixfix: bool -> string option -> mixfix -> mixfix * mixfix
+  val fork_mixfix: bool -> bool -> mixfix -> mixfix * mixfix
 
   val axclass_cmd: bstring * xstring list
     -> ((bstring * Attrib.src list) * string list) list
@@ -55,12 +55,12 @@
 
 (** auxiliary **)
 
-fun fork_mixfix is_loc some_class mx =
+fun fork_mixfix is_locale is_class mx =
   let
     val mx' = Syntax.unlocalize_mixfix mx;
-    val mx_global = if not is_loc orelse (is_some some_class andalso not (mx = mx'))
+    val mx_global = if not is_locale orelse (is_class andalso not (mx = mx'))
       then mx' else NoSyn;
-    val mx_local = if is_loc then mx else NoSyn;
+    val mx_local = if is_locale then mx else NoSyn;
   in (mx_global, mx_local) end;
 
 fun prove_interpretation tac prfx_atts expr inst =
@@ -718,7 +718,7 @@
       in
         (map fst params, params
         |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (Name.aT, local_sort)))
-        |> (map o apsnd) (fork_mixfix true (SOME "") #> fst)
+        |> (map o apsnd) (fork_mixfix true true #> fst)
         |> chop (length supconsts)
         |> snd)
       end;
@@ -802,7 +802,7 @@
     val ty'' = subst_typ ty';
     val c' = mk_name c;
     val def = (c, Logic.mk_equals (Const (c', ty'), rhs'));
-    val (syn', _) = fork_mixfix true (SOME class) syn;
+    val (syn', _) = fork_mixfix true true syn;
     fun interpret def thy =
       let
         val def' = symmetric def;