made sml/nj happy
authorpaulson
Thu Dec 16 12:05:00 2010 +0000 (2010-12-16)
changeset 41193dc33b8ea4526
parent 41169 95167879f675
child 41194 9796e5e01b61
made sml/nj happy
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/smt_translate.ML
src/HOL/Tools/SMT/z3_proof_parser.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Dec 15 17:14:44 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Thu Dec 16 12:05:00 2010 +0000
     1.3 @@ -586,7 +586,7 @@
     1.4    type T = extra_norm U.dict
     1.5    val empty = []
     1.6    val extend = I
     1.7 -  val merge = U.dict_merge fst
     1.8 +  fun merge xx = U.dict_merge fst xx
     1.9  )
    1.10  
    1.11  fun add_extra_norm (cs, norm) = Extra_Norms.map (U.dict_update (cs, norm))
     2.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 17:14:44 2010 +0100
     2.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Thu Dec 16 12:05:00 2010 +0000
     2.3 @@ -588,7 +588,7 @@
     2.4    type T = (Proof.context -> config) U.dict
     2.5    val empty = []
     2.6    val extend = I
     2.7 -  val merge = U.dict_merge fst
     2.8 +  fun merge xx = U.dict_merge fst xx
     2.9  )
    2.10  
    2.11  fun add_config (cs, cfg) = Configs.map (U.dict_update (cs, cfg))
     3.1 --- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Wed Dec 15 17:14:44 2010 +0100
     3.2 +++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Thu Dec 16 12:05:00 2010 +0000
     3.3 @@ -404,7 +404,7 @@
     3.4  val rule_arg = id
     3.5    (* if this is modified, then 'th_lemma_arg' needs reviewing *)
     3.6  
     3.7 -val th_lemma_arg = Scan.unless (sep rule_arg >> K "" || $$ rbra) (sep name)
     3.8 +fun th_lemma_arg st = Scan.unless (sep rule_arg >> K "" || $$ rbra) (sep name) st
     3.9  
    3.10  fun rule_name st = ((name >> `(Symtab.lookup rule_names)) :|-- (fn 
    3.11      (SOME (Th_Lemma _), _) => Scan.repeat th_lemma_arg >> Th_Lemma