Thm.fold_terms;
authorwenzelm
Sun Apr 15 14:31:47 2007 +0200 (2007-04-15)
changeset 22691290454649b8c
parent 22690 0b08f218f260
child 22692 1e057a3f087d
Thm.fold_terms;
src/HOL/Import/proof_kernel.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/res_axioms.ML
src/Pure/Isar/element.ML
src/Pure/Isar/local_defs.ML
src/Pure/axclass.ML
src/Pure/variable.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Sun Apr 15 14:31:44 2007 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Sun Apr 15 14:31:47 2007 +0200
     1.3 @@ -2199,9 +2199,9 @@
     1.4  		    [NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))]
     1.5                      typedef_hol2hollight
     1.6  	    val th4 = (#type_definition typedef_info) RS typedef_hol2hollight'
     1.7 -            val _ = null (Drule.fold_terms Term.add_tvars th4 []) orelse
     1.8 +            val _ = null (Thm.fold_terms Term.add_tvars th4 []) orelse
     1.9                raise ERR "type_introduction" "no type variables expected any more"
    1.10 -            val _ = null (Drule.fold_terms Term.add_vars th4 []) orelse
    1.11 +            val _ = null (Thm.fold_terms Term.add_vars th4 []) orelse
    1.12                raise ERR "type_introduction" "no term variables expected any more"
    1.13  	    val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname)
    1.14              val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
     2.1 --- a/src/HOL/Tools/datatype_realizer.ML	Sun Apr 15 14:31:44 2007 +0200
     2.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Sun Apr 15 14:31:47 2007 +0200
     2.3 @@ -136,7 +136,7 @@
     2.4        ||> Theory.restore_naming thy;
     2.5  
     2.6      val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []);
     2.7 -    val rvs = rev (Drule.fold_terms Term.add_vars thm' []);
     2.8 +    val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
     2.9      val ivs1 = map Var (filter_out (fn (_, T) =>
    2.10        tname_of (body_type T) mem ["set", "bool"]) ivs);
    2.11      val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (AList.lookup (op =) rvs ixn))) ivs;
     3.1 --- a/src/HOL/Tools/res_axioms.ML	Sun Apr 15 14:31:44 2007 +0200
     3.2 +++ b/src/HOL/Tools/res_axioms.ML	Sun Apr 15 14:31:47 2007 +0200
     3.3 @@ -152,7 +152,7 @@
     3.4  
     3.5  (*Returns the vars of a theorem*)
     3.6  fun vars_of_thm th =
     3.7 -  map (Thm.cterm_of (theory_of_thm th) o Var) (Drule.fold_terms Term.add_vars th []);
     3.8 +  map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
     3.9  
    3.10  (*Make a version of fun_cong with a given variable name*)
    3.11  local
     4.1 --- a/src/Pure/Isar/element.ML	Sun Apr 15 14:31:44 2007 +0200
     4.2 +++ b/src/Pure/Isar/element.ML	Sun Apr 15 14:31:47 2007 +0200
     4.3 @@ -374,7 +374,7 @@
     4.4  fun rename_thm ren th =
     4.5    let
     4.6      val thy = Thm.theory_of_thm th;
     4.7 -    val subst = (Drule.fold_terms o Term.fold_aterms)
     4.8 +    val subst = (Thm.fold_terms o Term.fold_aterms)
     4.9        (fn Free (x, T) =>
    4.10          let val x' = rename ren x
    4.11          in if x = x' then I else insert (eq_fst (op =)) ((x, T), Free (x', T)) end
    4.12 @@ -398,7 +398,7 @@
    4.13    if Symtab.is_empty env then I
    4.14    else Term.map_types (instT_type env);
    4.15  
    4.16 -fun instT_subst env th = (Drule.fold_terms o Term.fold_types o Term.fold_atyps)
    4.17 +fun instT_subst env th = (Thm.fold_terms o Term.fold_types o Term.fold_atyps)
    4.18    (fn T as TFree (a, _) =>
    4.19      let val T' = the_default T (Symtab.lookup env a)
    4.20      in if T = T' then I else insert (op =) (a, T') end
    4.21 @@ -443,7 +443,7 @@
    4.22    else
    4.23      let
    4.24        val substT = instT_subst envT th;
    4.25 -      val subst = (Drule.fold_terms o Term.fold_aterms)
    4.26 +      val subst = (Thm.fold_terms o Term.fold_aterms)
    4.27         (fn Free (x, T) =>
    4.28            let
    4.29              val T' = instT_type envT T;
     5.1 --- a/src/Pure/Isar/local_defs.ML	Sun Apr 15 14:31:44 2007 +0200
     5.2 +++ b/src/Pure/Isar/local_defs.ML	Sun Apr 15 14:31:47 2007 +0200
     5.3 @@ -109,7 +109,7 @@
     5.4    in fn th =>
     5.5      let
     5.6        val th' = exp th;
     5.7 -      val still_fixed = map #1 (Drule.fold_terms Term.add_frees th' []);
     5.8 +      val still_fixed = map #1 (Thm.fold_terms Term.add_frees th' []);
     5.9        val defs = prems |> filter_out (fn prem =>
    5.10          (case try (head_of_def o Thm.prop_of) prem of
    5.11            SOME x => member (op =) still_fixed x
     6.1 --- a/src/Pure/axclass.ML	Sun Apr 15 14:31:44 2007 +0200
     6.2 +++ b/src/Pure/axclass.ML	Sun Apr 15 14:31:47 2007 +0200
     6.3 @@ -214,7 +214,7 @@
     6.4  fun add_classrel th thy =
     6.5    let
     6.6      fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
     6.7 -    val prop = Drule.plain_prop_of (Thm.transfer thy th);
     6.8 +    val prop = Thm.plain_prop_of (Thm.transfer thy th);
     6.9      val rel = Logic.dest_classrel prop handle TERM _ => err ();
    6.10      val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
    6.11    in
    6.12 @@ -226,7 +226,7 @@
    6.13  fun add_arity th thy =
    6.14    let
    6.15      fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
    6.16 -    val prop = Drule.plain_prop_of (Thm.transfer thy th);
    6.17 +    val prop = Thm.plain_prop_of (Thm.transfer thy th);
    6.18      val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
    6.19      val _ = if map (Sign.certify_sort thy) Ss = Ss then () else err ();
    6.20    in
     7.1 --- a/src/Pure/variable.ML	Sun Apr 15 14:31:44 2007 +0200
     7.2 +++ b/src/Pure/variable.ML	Sun Apr 15 14:31:47 2007 +0200
     7.3 @@ -206,7 +206,7 @@
     7.4  
     7.5  val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
     7.6  
     7.7 -val declare_thm = Drule.fold_terms declare_internal;
     7.8 +val declare_thm = Thm.fold_terms declare_internal;
     7.9  fun thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th));
    7.10  
    7.11  
    7.12 @@ -444,7 +444,7 @@
    7.13  
    7.14  fun focus_subgoal i st =
    7.15    let
    7.16 -    val all_vars = Drule.fold_terms Term.add_vars st [];
    7.17 +    val all_vars = Thm.fold_terms Term.add_vars st [];
    7.18      val no_binds = map (fn (xi, _) => (xi, NONE)) all_vars;
    7.19    in
    7.20      add_binds no_binds #>