src/HOL/Tools/SMT/smt_normalize.ML
changeset 51575 907efc894051
parent 50601 74da81de127f
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Thu Mar 28 22:42:18 2013 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Thu Mar 28 23:44:41 2013 +0100
     1.3 @@ -571,11 +571,10 @@
     1.4      val (thms', extra_thms) = f thms
     1.5    in (is ~~ thms') @ map (pair ~1) extra_thms end
     1.6  
     1.7 -fun unfold2 ithms ctxt =
     1.8 +fun unfold2 ctxt ithms =
     1.9    ithms
    1.10    |> map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt)))
    1.11    |> burrow_ids add_nat_embedding
    1.12 -  |> rpair ctxt
    1.13  
    1.14  
    1.15  
    1.16 @@ -594,11 +593,11 @@
    1.17  fun add_extra_norm (cs, norm) =
    1.18    Extra_Norms.map (SMT_Utils.dict_update (cs, norm))
    1.19  
    1.20 -fun apply_extra_norms ithms ctxt =
    1.21 +fun apply_extra_norms ctxt ithms =
    1.22    let
    1.23      val cs = SMT_Config.solver_class_of ctxt
    1.24      val es = SMT_Utils.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
    1.25 -  in (burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms, ctxt) end
    1.26 +  in burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms end
    1.27  
    1.28  local
    1.29    val ignored = member (op =) [@{const_name All}, @{const_name Ex},
    1.30 @@ -622,12 +621,12 @@
    1.31      in (fn t => collect t Symtab.empty) end
    1.32  in
    1.33  
    1.34 -fun monomorph xthms ctxt =
    1.35 +fun monomorph ctxt xthms =
    1.36    let val (xs, thms) = split_list xthms
    1.37    in
    1.38 -    (map (pair 1) thms, ctxt)
    1.39 -    |-> Monomorph.monomorph schematic_consts_of
    1.40 -    |>> maps (uncurry (map o pair)) o map2 pair xs o map (map snd)
    1.41 +    map (pair 1) thms
    1.42 +    |> Monomorph.monomorph schematic_consts_of ctxt
    1.43 +    |> maps (uncurry (map o pair)) o map2 pair xs o map (map snd)
    1.44    end
    1.45  
    1.46  end
    1.47 @@ -636,10 +635,10 @@
    1.48    iwthms
    1.49    |> gen_normalize ctxt
    1.50    |> unfold1 ctxt
    1.51 +  |> monomorph ctxt
    1.52 +  |> unfold2 ctxt
    1.53 +  |> apply_extra_norms ctxt
    1.54    |> rpair ctxt
    1.55 -  |-> monomorph
    1.56 -  |-> unfold2
    1.57 -  |-> apply_extra_norms
    1.58  
    1.59  val setup = Context.theory_map (
    1.60    setup_atomize #>