src/HOL/Tools/TFL/post.ML
changeset 33832 cff42395c246
parent 33339 d41f77196338
child 35021 c839a4c670c6
     1.1 --- a/src/HOL/Tools/TFL/post.ML	Sat Nov 21 14:03:36 2009 +0100
     1.2 +++ b/src/HOL/Tools/TFL/post.ML	Sat Nov 21 15:49:29 2009 +0100
     1.3 @@ -27,7 +27,7 @@
     1.4   * have a tactic directly applied to them.
     1.5   *--------------------------------------------------------------------------*)
     1.6  fun termination_goals rules =
     1.7 -    map (Type.freeze o HOLogic.dest_Trueprop)
     1.8 +    map (Type.legacy_freeze o HOLogic.dest_Trueprop)
     1.9        (fold_rev (union (op aconv) o prems_of) rules []);
    1.10  
    1.11  (*---------------------------------------------------------------------------