moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
authorwenzelm
Wed Dec 31 18:53:16 2008 +0100 (2008-12-31)
changeset 292711d685baea08e
parent 29270 0eade173f77e
child 29272 fb3ccf499df5
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
use exists_Const directly;
src/HOL/Tools/inductive_realizer.ML
src/Pure/Proof/proof_rewrite_rules.ML
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Dec 31 18:53:16 2008 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Dec 31 18:53:16 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' (add_term_free_names (t, [])) [] t;
     1.8 +fun strip_all t = strip_all' (OldTerm.add_term_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 @@ -63,7 +63,7 @@
    1.13  
    1.14  fun dt_of_intrs thy vs nparms intrs =
    1.15    let
    1.16 -    val iTs = term_tvars (prop_of (hd intrs));
    1.17 +    val iTs = OldTerm.term_tvars (prop_of (hd intrs));
    1.18      val Tvs = map TVar iTs;
    1.19      val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
    1.20        (Logic.strip_imp_concl (prop_of (hd intrs))));
    1.21 @@ -100,7 +100,7 @@
    1.22  fun mk_realizes_eqn n vs nparms intrs =
    1.23    let
    1.24      val concl = HOLogic.dest_Trueprop (concl_of (hd intrs));
    1.25 -    val iTs = term_tvars concl;
    1.26 +    val iTs = OldTerm.term_tvars concl;
    1.27      val Tvs = map TVar iTs;
    1.28      val (h as Const (s, T), us) = strip_comb concl;
    1.29      val params = List.take (us, nparms);
    1.30 @@ -146,7 +146,7 @@
    1.31      val conclT = Extraction.etype_of thy vs [] (Logic.strip_imp_concl rule');
    1.32      val used = map (fst o dest_Free) args;
    1.33  
    1.34 -    fun is_rec t = not (null (term_consts t inter rsets));
    1.35 +    val is_rec = exists_Const (fn (c, _) => member (op =) rsets c);
    1.36  
    1.37      fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P
    1.38        | is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q
    1.39 @@ -275,7 +275,7 @@
    1.40    let
    1.41      val qualifier = NameSpace.qualifier (name_of_thm induct);
    1.42      val inducts = PureThy.get_thms thy (NameSpace.qualified qualifier "inducts");
    1.43 -    val iTs = term_tvars (prop_of (hd intrs));
    1.44 +    val iTs = OldTerm.term_tvars (prop_of (hd intrs));
    1.45      val ar = length vs + length iTs;
    1.46      val params = InductivePackage.params_of raw_induct;
    1.47      val arities = InductivePackage.arities_of raw_induct;
    1.48 @@ -370,7 +370,7 @@
    1.49            (vs' @ Ps) rec_names rss' intrs dummies;
    1.50          val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs' @ Ps) r
    1.51            (prop_of ind)) (rs ~~ inducts);
    1.52 -        val used = foldr add_term_free_names [] rlzs;
    1.53 +        val used = foldr OldTerm.add_term_free_names [] rlzs;
    1.54          val rnames = Name.variant_list used (replicate (length inducts) "r");
    1.55          val rnames' = Name.variant_list
    1.56            (used @ rnames) (replicate (length intrs) "s");
     2.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Wed Dec 31 18:53:16 2008 +0100
     2.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Wed Dec 31 18:53:16 2008 +0100
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      Pure/Proof/proof_rewrite_rules.ML
     2.5 -    ID:         $Id$
     2.6      Author:     Stefan Berghofer, TU Muenchen
     2.7  
     2.8  Simplification functions for proof terms involving meta level rules.
     2.9 @@ -196,7 +195,8 @@
    2.10    let
    2.11      fun rew_term Ts t =
    2.12        let
    2.13 -        val frees = map Free (Name.invent_list (add_term_names (t, [])) "xa" (length Ts) ~~ Ts);
    2.14 +        val frees =
    2.15 +          map Free (Name.invent_list (OldTerm.add_term_names (t, [])) "xa" (length Ts) ~~ Ts);
    2.16          val t' = r (subst_bounds (frees, t));
    2.17          fun strip [] t = t
    2.18            | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
    2.19 @@ -228,7 +228,7 @@
    2.20            if member (op =) defs s then
    2.21              let
    2.22                val vs = vars_of prop;
    2.23 -              val tvars = term_tvars prop;
    2.24 +              val tvars = OldTerm.term_tvars prop;
    2.25                val (_, rhs) = Logic.dest_equals prop;
    2.26                val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
    2.27                  (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
    2.28 @@ -249,7 +249,9 @@
    2.29          val cnames = map (fst o dest_Const o fst) defs';
    2.30          val thms = fold_proof_atoms true
    2.31            (fn PThm (_, ((name, prop, _), _)) =>
    2.32 -              if member (op =) defnames name orelse null (term_consts prop inter cnames) then I
    2.33 +              if member (op =) defnames name orelse
    2.34 +                not (exists_Const (member (op =) cnames o #1) prop)
    2.35 +              then I
    2.36                else cons (name, SOME prop)
    2.37              | _ => I) [prf] [];
    2.38        in Reconstruct.expand_proof thy thms end;