src/Pure/meta_simplifier.ML
changeset 15249 0da6b3075bfa
parent 15199 29ca1fe63e7b
child 15460 dd48bf51aff1
     1.1 --- a/src/Pure/meta_simplifier.ML	Fri Oct 15 18:49:16 2004 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Mon Oct 18 11:43:40 2004 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4    val rep_ss: simpset ->
     1.5     {rules: rrule Net.net,
     1.6      prems: thm list,
     1.7 -    bounds: string list,
     1.8 +    bounds: int,
     1.9      depth: int} *
    1.10     {congs: (string * cong) list * string list,
    1.11      procs: proc Net.net,
    1.12 @@ -193,7 +193,7 @@
    1.13  (*A simpset contains data required during conversion:
    1.14      rules: discrimination net of rewrite rules;
    1.15      prems: current premises;
    1.16 -    bounds: names of bound variables already used
    1.17 +    bounds: maximal index of bound variables already used
    1.18        (for generating new names when rewriting under lambda abstractions);
    1.19      depth: depth of conditional rewriting;
    1.20      congs: association list of congruence rules and
    1.21 @@ -218,7 +218,7 @@
    1.22    Simpset of
    1.23     {rules: rrule Net.net,
    1.24      prems: thm list,
    1.25 -    bounds: string list,
    1.26 +    bounds: int,
    1.27      depth: int} *
    1.28     {congs: (string * cong) list * string list,
    1.29      procs: proc Net.net,
    1.30 @@ -297,7 +297,7 @@
    1.31  local
    1.32  
    1.33  fun init_ss mk_rews termless subgoal_tac solvers =
    1.34 -  make_simpset ((Net.empty, [], [], 0),
    1.35 +  make_simpset ((Net.empty, [], 0, 0),
    1.36      (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
    1.37  
    1.38  val basic_mk_rews: mk_rews =
    1.39 @@ -329,7 +329,7 @@
    1.40  
    1.41      val rules' = Net.merge (rules1, rules2, eq_rrule);
    1.42      val prems' = gen_merge_lists Drule.eq_thm_prop prems1 prems2;
    1.43 -    val bounds' = merge_lists bounds1 bounds2;
    1.44 +    val bounds' = Int.max (bounds1, bounds2);
    1.45      val congs' = gen_merge_lists (eq_cong o pairself #2) congs1 congs2;
    1.46      val weak' = merge_lists weak1 weak2;
    1.47      val procs' = Net.merge (procs1, procs2, eq_proc);
    1.48 @@ -363,8 +363,8 @@
    1.49  
    1.50  (* bounds and prems *)
    1.51  
    1.52 -fun add_bound b = map_simpset1 (fn (rules, prems, bounds, depth) =>
    1.53 -  (rules, prems, b :: bounds, depth));
    1.54 +val incr_bounds = map_simpset1 (fn (rules, prems, bounds, depth) =>
    1.55 +  (rules, prems, bounds + 1, depth));
    1.56  
    1.57  fun add_prems ths = map_simpset1 (fn (rules, prems, bounds, depth) =>
    1.58    (rules, ths @ prems, bounds, depth));
    1.59 @@ -928,9 +928,8 @@
    1.60         (case term_of t0 of
    1.61             Abs (a, T, t) =>
    1.62               let
    1.63 -                 val b = variant bounds a;
    1.64 -                 val (v, t') = Thm.dest_abs (Some ("." ^ b)) t0;
    1.65 -                 val ss' = add_bound b ss;
    1.66 +                 val (v, t') = Thm.dest_abs (Some ("." ^ a ^ "." ^ string_of_int bounds)) t0;
    1.67 +                 val ss' = incr_bounds ss;
    1.68                   val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;
    1.69               in case botc skel' ss' t' of
    1.70                    Some thm => Some (abstract_rule a v thm)