src/Pure/Isar/local_defs.ML
changeset 22691 290454649b8c
parent 22671 3c62305fbee6
child 22846 fb79144af9a3
     1.1 --- a/src/Pure/Isar/local_defs.ML	Sun Apr 15 14:31:44 2007 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Sun Apr 15 14:31:47 2007 +0200
     1.3 @@ -109,7 +109,7 @@
     1.4    in fn th =>
     1.5      let
     1.6        val th' = exp th;
     1.7 -      val still_fixed = map #1 (Drule.fold_terms Term.add_frees th' []);
     1.8 +      val still_fixed = map #1 (Thm.fold_terms Term.add_frees th' []);
     1.9        val defs = prems |> filter_out (fn prem =>
    1.10          (case try (head_of_def o Thm.prop_of) prem of
    1.11            SOME x => member (op =) still_fixed x