src/HOL/Nominal/nominal_fresh_fun.ML
changeset 29265 5b4247055bd7
parent 28397 389c5e494605
child 30280 eb98b49ef835
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Dec 31 00:08:11 2008 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Dec 31 00:08:13 2008 +0100
     1.3 @@ -1,10 +1,8 @@
     1.4  (*  Title:      HOL/Nominal/nominal_fresh_fun.ML
     1.5 -    ID:         $Id$
     1.6 -    Authors:    Stefan Berghofer, Julien Narboux, TU Muenchen
     1.7 +    Authors:    Stefan Berghofer and Julien Narboux, TU Muenchen
     1.8  
     1.9  Provides a tactic to generate fresh names and
    1.10  a tactic to analyse instances of the fresh_fun.
    1.11 -
    1.12  *)
    1.13  
    1.14  (* First some functions that should be in the library *)
    1.15 @@ -83,7 +81,7 @@
    1.16     val bvs = map_index (Bound o fst) ps;
    1.17  (* select variables of the right class *)
    1.18     val vs = filter (fn t => is_of_fs_name (fastype_of1 (Ts, t)))
    1.19 -     (term_frees goal @ bvs);
    1.20 +     (OldTerm.term_frees goal @ bvs);
    1.21  (* build the tuple *)
    1.22     val s = (Library.foldr1 (fn (v, s) =>
    1.23       HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) vs) handle _ => HOLogic.unit ;  (* FIXME avoid handle _ *)
    1.24 @@ -91,7 +89,7 @@
    1.25     val at_name_inst_thm = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
    1.26     val exists_fresh' = at_name_inst_thm RS at_exists_fresh';
    1.27  (* find the variable we want to instantiate *)
    1.28 -   val x = hd (term_vars (prop_of exists_fresh'));
    1.29 +   val x = hd (OldTerm.term_vars (prop_of exists_fresh'));
    1.30   in 
    1.31     (cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN
    1.32     rtac fs_name_thm 1 THEN
    1.33 @@ -150,7 +148,7 @@
    1.34      val fresh_perm_app = PureThy.get_thms thy "fresh_perm_app";
    1.35      val ss' = ss addsimps fresh_prod::abs_fresh;
    1.36      val ss'' = ss' addsimps fresh_perm_app;
    1.37 -    val x = hd (tl (term_vars (prop_of exI)));
    1.38 +    val x = hd (tl (OldTerm.term_vars (prop_of exI)));
    1.39      val goal = nth (prems_of thm) (i-1);
    1.40      val atom_name_opt = get_inner_fresh_fun goal;
    1.41      val n = List.length (Logic.strip_params goal);
    1.42 @@ -165,7 +163,7 @@
    1.43      val pt_name_inst = get_dyn_thm thy ("pt_"^atom_basename^"_inst") atom_basename;
    1.44      val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
    1.45      fun inst_fresh vars params i st =
    1.46 -   let val vars' = term_vars (prop_of st);
    1.47 +   let val vars' = OldTerm.term_vars (prop_of st);
    1.48         val thy = theory_of_thm st;
    1.49     in case vars' \\ vars of 
    1.50       [x] => Seq.single (Thm.instantiate ([],[(cterm_of thy x,cterm_of thy (list_abs (params,Bound 0)))]) st)
    1.51 @@ -174,7 +172,7 @@
    1.52    in
    1.53    ((fn st =>
    1.54    let 
    1.55 -    val vars = term_vars (prop_of st);
    1.56 +    val vars = OldTerm.term_vars (prop_of st);
    1.57      val params = Logic.strip_params (nth (prems_of st) (i-1))
    1.58      (* The tactics which solve the subgoals generated 
    1.59         by the conditionnal rewrite rule. *)