changeset 49985 | 5b4b0e4e5205 |
parent 49983 | 33e18e9916a8 |
child 51552 | c713c9505f68 |
--- a/src/HOL/TPTP/atp_problem_import.ML Wed Oct 31 11:23:21 2012 +0100 +++ b/src/HOL/TPTP/atp_problem_import.ML Wed Oct 31 11:23:21 2012 +0100 @@ -72,7 +72,7 @@ val thy = Proof_Context.theory_of ctxt val (defs, pseudo_defs) = defs |> map (ATP_Util.abs_extensionalize_term ctxt - #> aptrueprop (open_form I)) + #> aptrueprop (hol_open_form I)) |> List.partition (ATP_Util.is_legitimate_tptp_def o perhaps (try HOLogic.dest_Trueprop) o ATP_Util.unextensionalize_def)