src/HOL/Tools/inductive_realizer.ML
changeset 29281 b22ccb3998db
parent 29271 1d685baea08e
child 29389 0a49f940d729
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Dec 31 19:56:38 2008 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Dec 31 20:31:36 2008 +0100
     1.3 @@ -49,7 +49,7 @@
     1.4        t $ strip_all' used names Q
     1.5    | strip_all' _ _ t = t;
     1.6  
     1.7 -fun strip_all t = strip_all' (OldTerm.add_term_free_names (t, [])) [] t;
     1.8 +fun strip_all t = strip_all' (Term.add_free_names t []) [] t;
     1.9  
    1.10  fun strip_one name (Const ("all", _) $ Abs (s, T, Const ("==>", _) $ P $ Q)) =
    1.11        (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
    1.12 @@ -370,7 +370,7 @@
    1.13            (vs' @ Ps) rec_names rss' intrs dummies;
    1.14          val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs' @ Ps) r
    1.15            (prop_of ind)) (rs ~~ inducts);
    1.16 -        val used = foldr OldTerm.add_term_free_names [] rlzs;
    1.17 +        val used = fold Term.add_free_names rlzs [];
    1.18          val rnames = Name.variant_list used (replicate (length inducts) "r");
    1.19          val rnames' = Name.variant_list
    1.20            (used @ rnames) (replicate (length intrs) "s");