--- a/src/HOL/Tools/SMT/smt_normalize.ML Thu Dec 16 13:34:28 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Thu Dec 16 13:54:17 2010 +0100
@@ -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))
--- a/src/HOL/Tools/SMT/smt_translate.ML Thu Dec 16 13:34:28 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML Thu Dec 16 13:54:17 2010 +0100
@@ -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))
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML Thu Dec 16 13:34:28 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML Thu Dec 16 13:54:17 2010 +0100
@@ -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