# HG changeset patch # User boehmes # Date 1292504057 -3600 # Node ID aa627a799e8e9bbc375ae133f288ee7c56dbbd50 # Parent edab1efe0a7086d1668ab9d107f123b273248e70# Parent 9796e5e01b61e2aa6bacc32a4073ceda7070de4c merged diff -r edab1efe0a70 -r aa627a799e8e src/HOL/Tools/SMT/smt_normalize.ML --- 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)) diff -r edab1efe0a70 -r aa627a799e8e src/HOL/Tools/SMT/smt_translate.ML --- 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)) diff -r edab1efe0a70 -r aa627a799e8e src/HOL/Tools/SMT/z3_proof_parser.ML --- 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