src/HOL/Tools/SMT2/smt2_normalize.ML
changeset 56106 9cfea3ab002a
parent 56105 75dc126f5dcb
child 56107 2ec2d06b9424
     1.1 --- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Mar 13 14:48:20 2014 +0100
     1.2 +++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Mar 13 14:48:20 2014 +0100
     1.3 @@ -10,8 +10,7 @@
     1.4    val atomize_conv: Proof.context -> conv
     1.5    type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
     1.6    val add_extra_norm: SMT2_Util.class * extra_norm -> Context.generic -> Context.generic
     1.7 -  val normalize: (int * (int option * thm)) list -> Proof.context ->
     1.8 -    (int * thm) list * Proof.context
     1.9 +  val normalize: Proof.context -> (int option * thm) list -> (int * thm) list
    1.10  end
    1.11  
    1.12  structure SMT2_Normalize: SMT2_NORMALIZE =
    1.13 @@ -497,7 +496,7 @@
    1.14    let
    1.15      val (is, thms) = split_list ithms
    1.16      val (thms', extra_thms) = f thms
    1.17 -  in (is ~~ thms') @ tag_list (fold Integer.max is 0 + 1) extra_thms end
    1.18 +  in (is ~~ thms') @ map (pair ~1) extra_thms end
    1.19  
    1.20  fun unfold2 ctxt ithms =
    1.21    ithms
    1.22 @@ -558,14 +557,14 @@
    1.23  
    1.24  end
    1.25  
    1.26 -fun normalize iwthms ctxt =
    1.27 -  iwthms
    1.28 +fun normalize ctxt wthms =
    1.29 +  wthms
    1.30 +  |> map_index I
    1.31    |> gen_normalize ctxt
    1.32    |> unfold1 ctxt
    1.33    |> monomorph ctxt
    1.34    |> unfold2 ctxt
    1.35    |> apply_extra_norms ctxt
    1.36 -  |> rpair ctxt
    1.37  
    1.38  val _ = Theory.setup (Context.theory_map (
    1.39    setup_atomize #>