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;