src/HOL/Tools/SMT/smt_normalize.ML
changeset 40162 7f58a9a843c2
parent 40161 539d07b00e5f
child 40274 6486c610a549
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue Oct 26 11:39:26 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Oct 26 11:45:12 2010 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  
     1.5  signature SMT_NORMALIZE =
     1.6  sig
     1.7 -  type extra_norm = (int * thm) list -> Proof.context ->
     1.8 +  type extra_norm = bool -> (int * thm) list -> Proof.context ->
     1.9      (int * thm) list * Proof.context
    1.10    val normalize: extra_norm -> bool -> (int * thm) list -> Proof.context ->
    1.11      (int * thm) list * Proof.context
    1.12 @@ -480,7 +480,7 @@
    1.13  
    1.14  (* combined normalization *)
    1.15  
    1.16 -type extra_norm = (int * thm) list -> Proof.context ->
    1.17 +type extra_norm = bool -> (int * thm) list -> Proof.context ->
    1.18    (int * thm) list * Proof.context
    1.19  
    1.20  fun with_context f irules ctxt = (f ctxt irules, ctxt)
    1.21 @@ -492,7 +492,7 @@
    1.22    |> normalize_numerals ctxt
    1.23    |> nat_as_int ctxt
    1.24    |> rpair ctxt
    1.25 -  |-> extra_norm
    1.26 +  |-> extra_norm with_datatypes
    1.27    |-> with_context (fn cx => map (apsnd (normalize_rule cx)))
    1.28    |-> SMT_Monomorph.monomorph
    1.29    |-> lift_lambdas