# HG changeset patch
# User boehmes
# Date 1292829443 -3600
# Node ID 528f5d00b5428816dc13dd362d01505cd97b6cd4
# Parent  01b2de947cff28b62c4ea60c3bab6d0b11408590
perform monomorphization during normalization: schematic numerals might be monomorphized into built-in numerals and then numeral normalization is required

diff -r 01b2de947cff -r 528f5d00b542 src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Sun Dec 19 18:38:50 2010 -0800
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Mon Dec 20 08:17:23 2010 +0100
@@ -10,8 +10,8 @@
   type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
   val add_extra_norm: SMT_Utils.class * extra_norm -> Context.generic ->
     Context.generic
-  val normalize: Proof.context -> (int * (int option * thm)) list ->
-    (int * thm) list
+  val normalize: (int * (int option * thm)) list -> Proof.context ->
+    (int * thm) list * Proof.context
   val setup: theory -> theory
 end
 
@@ -574,17 +574,21 @@
   rewrite_bool_case_conv ctxt then_conv
   unfold_abs_min_max_conv ctxt then_conv
   nat_as_int_conv ctxt then_conv
-  normalize_numerals_conv ctxt then_conv
   Thm.beta_conversion true
 
+fun unfold1 ctxt = map (apsnd (Conv.fconv_rule (unfold_conv ctxt)))
+
 fun burrow_ids f ithms =
   let
     val (is, thms) = split_list ithms
     val (thms', extra_thms) = f thms
   in (is ~~ thms') @ map (pair ~1) extra_thms end
 
-fun unfold ctxt =
-  burrow_ids (map (Conv.fconv_rule (unfold_conv ctxt)) #> add_nat_embedding)
+fun unfold2 ithms ctxt =
+  ithms
+  |> map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt)))
+  |> burrow_ids add_nat_embedding
+  |> rpair ctxt
 
 
 
@@ -602,17 +606,20 @@
 
 fun add_extra_norm (cs, norm) = Extra_Norms.map (U.dict_update (cs, norm))
 
-fun apply_extra_norms ctxt =
+fun apply_extra_norms ithms ctxt =
   let
     val cs = SMT_Config.solver_class_of ctxt
     val es = U.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
-  in burrow_ids (fold (fn e => e ctxt) es o rpair []) end
+  in (burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms, ctxt) end
 
-fun normalize ctxt iwthms =
+fun normalize iwthms ctxt =
   iwthms
   |> gen_normalize ctxt
-  |> unfold ctxt
-  |> apply_extra_norms ctxt
+  |> unfold1 ctxt
+  |> rpair ctxt
+  |-> SMT_Monomorph.monomorph
+  |-> unfold2
+  |-> apply_extra_norms
 
 val setup = Context.theory_map (
   setup_atomize #>
diff -r 01b2de947cff -r 528f5d00b542 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Sun Dec 19 18:38:50 2010 -0800
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon Dec 20 08:17:23 2010 +0100
@@ -214,10 +214,7 @@
     int list * thm,
   default_max_relevant: int }
 
-fun gen_solver_head ctxt iwthms =
-  SMT_Normalize.normalize ctxt iwthms
-  |> rpair ctxt
-  |-> SMT_Monomorph.monomorph
+fun gen_solver_head ctxt iwthms = SMT_Normalize.normalize iwthms ctxt
 
 fun gen_solver_tail (name, info : solver_info) rm (iwthms', ctxt) iwthms =
   let