# HG changeset patch
# User paulson
# Date 1292501100 0
# Node ID dc33b8ea45269af367a5a44b6cdc9b8b8be00bb7
# Parent  95167879f67526b78d461d8575bce6a923eae50d
made sml/nj happy

diff -r 95167879f675 -r dc33b8ea4526 src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Dec 15 17:14:44 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Thu Dec 16 12:05:00 2010 +0000
@@ -586,7 +586,7 @@
   type T = extra_norm U.dict
   val empty = []
   val extend = I
-  val merge = U.dict_merge fst
+  fun merge xx = U.dict_merge fst xx
 )
 
 fun add_extra_norm (cs, norm) = Extra_Norms.map (U.dict_update (cs, norm))
diff -r 95167879f675 -r dc33b8ea4526 src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 17:14:44 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Thu Dec 16 12:05:00 2010 +0000
@@ -588,7 +588,7 @@
   type T = (Proof.context -> config) U.dict
   val empty = []
   val extend = I
-  val merge = U.dict_merge fst
+  fun merge xx = U.dict_merge fst xx
 )
 
 fun add_config (cs, cfg) = Configs.map (U.dict_update (cs, cfg))
diff -r 95167879f675 -r dc33b8ea4526 src/HOL/Tools/SMT/z3_proof_parser.ML
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Wed Dec 15 17:14:44 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Thu Dec 16 12:05:00 2010 +0000
@@ -404,7 +404,7 @@
 val rule_arg = id
   (* if this is modified, then 'th_lemma_arg' needs reviewing *)
 
-val th_lemma_arg = Scan.unless (sep rule_arg >> K "" || $$ rbra) (sep name)
+fun th_lemma_arg st = Scan.unless (sep rule_arg >> K "" || $$ rbra) (sep name) st
 
 fun rule_name st = ((name >> `(Symtab.lookup rule_names)) :|-- (fn 
     (SOME (Th_Lemma _), _) => Scan.repeat th_lemma_arg >> Th_Lemma