| changeset 42183 | 173b0f488428 |
| parent 41328 | 6792a5c92a58 |
| child 42190 | b6b5846504cd |
--- a/src/HOL/Tools/SMT/smt_normalize.ML Thu Mar 31 11:16:54 2011 +0200 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Thu Mar 31 14:02:03 2011 +0200 @@ -631,7 +631,7 @@ |> gen_normalize ctxt |> unfold1 ctxt |> rpair ctxt - |-> SMT_Monomorph.monomorph + |-> SMT_Monomorph.monomorph true |-> unfold2 |-> apply_extra_norms