# HG changeset patch
# User haftmann
# Date 1150814790 -7200
# Node ID 63bd0eeb4e0d0179f5ae3388b7a4360b445e205b
# Parent  fb32b43e7f80f38767ec5b079572319869d8b798
fixed sml/nj value restriction problem

diff -r fb32b43e7f80 -r 63bd0eeb4e0d src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Jun 20 15:53:44 2006 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Jun 20 16:46:30 2006 +0200
@@ -542,8 +542,8 @@
     val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
   in map (Option.map (Envir.norm_type unifier')) Vs end;
 
-fun params_of elemss = distinct (eq_fst (op =)) (maps (snd o fst) elemss);
-fun params_of' elemss = distinct (eq_fst (op =)) (maps (snd o fst o fst) elemss);
+fun params_of elemss = distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst) elemss);
+fun params_of' elemss = distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
 fun params_syn_of syn elemss =
   distinct (eq_fst (op =)) (maps (snd o fst) elemss) |>
     map (apfst (fn x => (x, the (Symtab.lookup syn x))));
@@ -554,7 +554,7 @@
 fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;
 
 
-fun merge_syntax ctxt ids ss = Symtab.merge (op =) ss
+fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix -> bool) ss
   handle Symtab.DUPS xs => err_in_locale ctxt
     ("Conflicting syntax for parameter(s): " ^ commas_quote xs) (map fst ids);
 
@@ -664,7 +664,7 @@
         end;
 
     fun merge_syn expr syn1 syn2 =
-        Symtab.merge (op =) (syn1, syn2)
+        Symtab.merge (op = : mixfix * mixfix -> bool) (syn1, syn2)
         handle Symtab.DUPS xs => err_in_expr ctxt
           ("Conflicting syntax for parameter(s): " ^ commas_quote xs) expr;
             
@@ -1177,7 +1177,7 @@
    If so, which are these??? *)
 
 fun finish_parms parms (((name, ps), mode), elems) =
-  (((name, map (fn (x, _) => (x, AList.lookup (op =) parms x)) ps), mode), elems);
+  (((name, map (fn (x, _) => (x, AList.lookup (op = : string * string -> bool) parms x)) ps), mode), elems);
 
 fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) =
       let
@@ -1445,8 +1445,8 @@
 val read_expr = prep_expr read_context;
 val cert_expr = prep_expr cert_context;
 
-val read_context_statement = prep_statement intern read_ctxt;
-val cert_context_statement = prep_statement (K I) cert_ctxt;
+fun read_context_statement raw_locale = prep_statement intern read_ctxt raw_locale ;
+fun cert_context_statement raw_locale = prep_statement (K I) cert_ctxt raw_locale ;
 
 end;