fixed sml/nj value restriction problem
authorhaftmann
Tue Jun 20 16:46:30 2006 +0200 (2006-06-20)
changeset 1993263bd0eeb4e0d
parent 19931 fb32b43e7f80
child 19933 16a5037f2d25
fixed sml/nj value restriction problem
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Tue Jun 20 15:53:44 2006 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Tue Jun 20 16:46:30 2006 +0200
     1.3 @@ -542,8 +542,8 @@
     1.4      val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
     1.5    in map (Option.map (Envir.norm_type unifier')) Vs end;
     1.6  
     1.7 -fun params_of elemss = distinct (eq_fst (op =)) (maps (snd o fst) elemss);
     1.8 -fun params_of' elemss = distinct (eq_fst (op =)) (maps (snd o fst o fst) elemss);
     1.9 +fun params_of elemss = distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst) elemss);
    1.10 +fun params_of' elemss = distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
    1.11  fun params_syn_of syn elemss =
    1.12    distinct (eq_fst (op =)) (maps (snd o fst) elemss) |>
    1.13      map (apfst (fn x => (x, the (Symtab.lookup syn x))));
    1.14 @@ -554,7 +554,7 @@
    1.15  fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;
    1.16  
    1.17  
    1.18 -fun merge_syntax ctxt ids ss = Symtab.merge (op =) ss
    1.19 +fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix -> bool) ss
    1.20    handle Symtab.DUPS xs => err_in_locale ctxt
    1.21      ("Conflicting syntax for parameter(s): " ^ commas_quote xs) (map fst ids);
    1.22  
    1.23 @@ -664,7 +664,7 @@
    1.24          end;
    1.25  
    1.26      fun merge_syn expr syn1 syn2 =
    1.27 -        Symtab.merge (op =) (syn1, syn2)
    1.28 +        Symtab.merge (op = : mixfix * mixfix -> bool) (syn1, syn2)
    1.29          handle Symtab.DUPS xs => err_in_expr ctxt
    1.30            ("Conflicting syntax for parameter(s): " ^ commas_quote xs) expr;
    1.31              
    1.32 @@ -1177,7 +1177,7 @@
    1.33     If so, which are these??? *)
    1.34  
    1.35  fun finish_parms parms (((name, ps), mode), elems) =
    1.36 -  (((name, map (fn (x, _) => (x, AList.lookup (op =) parms x)) ps), mode), elems);
    1.37 +  (((name, map (fn (x, _) => (x, AList.lookup (op = : string * string -> bool) parms x)) ps), mode), elems);
    1.38  
    1.39  fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) =
    1.40        let
    1.41 @@ -1445,8 +1445,8 @@
    1.42  val read_expr = prep_expr read_context;
    1.43  val cert_expr = prep_expr cert_context;
    1.44  
    1.45 -val read_context_statement = prep_statement intern read_ctxt;
    1.46 -val cert_context_statement = prep_statement (K I) cert_ctxt;
    1.47 +fun read_context_statement raw_locale = prep_statement intern read_ctxt raw_locale ;
    1.48 +fun cert_context_statement raw_locale = prep_statement (K I) cert_ctxt raw_locale ;
    1.49  
    1.50  end;
    1.51