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