fork_mixfix: explicit bool argument;
authorwenzelm
Fri Oct 12 20:21:56 2007 +0200 (2007-10-12)
changeset 250108bc74ba1423d
parent 25009 61946780de00
child 25011 633afd909ff2
fork_mixfix: explicit bool argument;
src/Pure/Isar/class.ML
     1.1 --- a/src/Pure/Isar/class.ML	Fri Oct 12 18:09:12 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Oct 12 20:21:56 2007 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature CLASS =
     1.6  sig
     1.7 -  val fork_mixfix: bool -> string option -> mixfix -> mixfix * mixfix
     1.8 +  val fork_mixfix: bool -> bool -> mixfix -> mixfix * mixfix
     1.9  
    1.10    val axclass_cmd: bstring * xstring list
    1.11      -> ((bstring * Attrib.src list) * string list) list
    1.12 @@ -55,12 +55,12 @@
    1.13  
    1.14  (** auxiliary **)
    1.15  
    1.16 -fun fork_mixfix is_loc some_class mx =
    1.17 +fun fork_mixfix is_locale is_class mx =
    1.18    let
    1.19      val mx' = Syntax.unlocalize_mixfix mx;
    1.20 -    val mx_global = if not is_loc orelse (is_some some_class andalso not (mx = mx'))
    1.21 +    val mx_global = if not is_locale orelse (is_class andalso not (mx = mx'))
    1.22        then mx' else NoSyn;
    1.23 -    val mx_local = if is_loc then mx else NoSyn;
    1.24 +    val mx_local = if is_locale then mx else NoSyn;
    1.25    in (mx_global, mx_local) end;
    1.26  
    1.27  fun prove_interpretation tac prfx_atts expr inst =
    1.28 @@ -718,7 +718,7 @@
    1.29        in
    1.30          (map fst params, params
    1.31          |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (Name.aT, local_sort)))
    1.32 -        |> (map o apsnd) (fork_mixfix true (SOME "") #> fst)
    1.33 +        |> (map o apsnd) (fork_mixfix true true #> fst)
    1.34          |> chop (length supconsts)
    1.35          |> snd)
    1.36        end;
    1.37 @@ -802,7 +802,7 @@
    1.38      val ty'' = subst_typ ty';
    1.39      val c' = mk_name c;
    1.40      val def = (c, Logic.mk_equals (Const (c', ty'), rhs'));
    1.41 -    val (syn', _) = fork_mixfix true (SOME class) syn;
    1.42 +    val (syn', _) = fork_mixfix true true syn;
    1.43      fun interpret def thy =
    1.44        let
    1.45          val def' = symmetric def;