src/HOL/Nominal/nominal_fresh_fun.ML
changeset 44121 44adaa6db327
parent 43278 1fbdcebb364b
child 46219 426ed18eba43
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Aug 10 20:12:36 2011 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Aug 10 20:53:43 2011 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4     val bvs = map_index (Bound o fst) ps;
     1.5  (* select variables of the right class *)
     1.6     val vs = filter (fn t => is_of_fs_name (fastype_of1 (Ts, t)))
     1.7 -     (OldTerm.term_frees goal @ bvs);
     1.8 +     (Misc_Legacy.term_frees goal @ bvs);
     1.9  (* build the tuple *)
    1.10     val s = (Library.foldr1 (fn (v, s) =>
    1.11         HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) vs)
    1.12 @@ -78,7 +78,7 @@
    1.13     val at_name_inst_thm = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
    1.14     val exists_fresh' = at_name_inst_thm RS at_exists_fresh';
    1.15  (* find the variable we want to instantiate *)
    1.16 -   val x = hd (OldTerm.term_vars (prop_of exists_fresh'));
    1.17 +   val x = hd (Misc_Legacy.term_vars (prop_of exists_fresh'));
    1.18   in
    1.19     (cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN
    1.20     rtac fs_name_thm 1 THEN
    1.21 @@ -137,7 +137,7 @@
    1.22      val fresh_perm_app = Global_Theory.get_thms thy "fresh_perm_app";
    1.23      val ss' = ss addsimps fresh_prod::abs_fresh;
    1.24      val ss'' = ss' addsimps fresh_perm_app;
    1.25 -    val x = hd (tl (OldTerm.term_vars (prop_of exI)));
    1.26 +    val x = hd (tl (Misc_Legacy.term_vars (prop_of exI)));
    1.27      val goal = nth (prems_of thm) (i-1);
    1.28      val atom_name_opt = get_inner_fresh_fun goal;
    1.29      val n = length (Logic.strip_params goal);
    1.30 @@ -152,7 +152,7 @@
    1.31      val pt_name_inst = get_dyn_thm thy ("pt_"^atom_basename^"_inst") atom_basename;
    1.32      val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
    1.33      fun inst_fresh vars params i st =
    1.34 -   let val vars' = OldTerm.term_vars (prop_of st);
    1.35 +   let val vars' = Misc_Legacy.term_vars (prop_of st);
    1.36         val thy = theory_of_thm st;
    1.37     in case subtract (op =) vars vars' of
    1.38       [x] => Seq.single (Thm.instantiate ([],[(cterm_of thy x,cterm_of thy (list_abs (params,Bound 0)))]) st)
    1.39 @@ -161,7 +161,7 @@
    1.40    in
    1.41    ((fn st =>
    1.42    let
    1.43 -    val vars = OldTerm.term_vars (prop_of st);
    1.44 +    val vars = Misc_Legacy.term_vars (prop_of st);
    1.45      val params = Logic.strip_params (nth (prems_of st) (i-1))
    1.46      (* The tactics which solve the subgoals generated
    1.47         by the conditionnal rewrite rule. *)