# HG changeset patch
# User paulson
# Date 1292501940 0
# Node ID 9796e5e01b61e2aa6bacc32a4073ceda7070de4c
# Parent  8aace46ffecb3828bf544641cf317b9a999b90dc# Parent  dc33b8ea45269af367a5a44b6cdc9b8b8be00bb7
merged

diff -r 8aace46ffecb -r 9796e5e01b61 src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Thu Dec 16 11:31:22 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Thu Dec 16 12:19:00 2010 +0000
@@ -589,7 +589,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 8aace46ffecb -r 9796e5e01b61 src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Thu Dec 16 11:31:22 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Thu Dec 16 12:19:00 2010 +0000
@@ -581,7 +581,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 8aace46ffecb -r 9796e5e01b61 src/HOL/Tools/SMT/z3_proof_parser.ML
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Thu Dec 16 11:31:22 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Thu Dec 16 12:19: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