--- 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;