changeset 42190 | b6b5846504cd |
parent 42183 | 173b0f488428 |
child 42361 | 23f352990944 |
--- a/src/HOL/Tools/SMT/smt_normalize.ML Fri Apr 01 10:18:20 2011 +0200 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Fri Apr 01 11:54:51 2011 +0200 @@ -631,7 +631,7 @@ |> gen_normalize ctxt |> unfold1 ctxt |> rpair ctxt - |-> SMT_Monomorph.monomorph true + |-> SMT_Monomorph.monomorph |-> unfold2 |-> apply_extra_norms