changeset 47953 | a2c3706c4cb1 |
parent 47946 | 33afcfad3f8d |
child 47954 | aada9fd08b58 |
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon May 21 16:37:28 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue May 22 16:59:27 2012 +0200 @@ -1272,7 +1272,7 @@ val is_ho = is_type_enc_higher_order type_enc in t |> need_trueprop ? HOLogic.mk_Trueprop - |> (if is_ho then unextensionalize_def else extensionalize_term ctxt) + |> (if is_ho then unextensionalize_def else abs_extensionalize_term ctxt) |> presimplify_term thy |> HOLogic.dest_Trueprop end