Thm.adjust_maxidx;
authorwenzelm
Sun Jul 30 21:28:52 2006 +0200 (2006-07-30)
changeset 20260990dbc007ca6
parent 20259 5eda3b38ec90
child 20261 af51389aa756
Thm.adjust_maxidx;
src/Pure/axclass.ML
src/Pure/conjunction.ML
src/Pure/drule.ML
src/Pure/goal.ML
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/axclass.ML	Sun Jul 30 21:28:51 2006 +0200
     1.2 +++ b/src/Pure/axclass.ML	Sun Jul 30 21:28:52 2006 +0200
     1.3 @@ -425,7 +425,7 @@
     1.4        sort |> map (fn c =>
     1.5          Goal.finish (the (lookup_type cache' typ c) RS
     1.6            Goal.init (Thm.cterm_of thy (Logic.mk_inclass (typ, c))))
     1.7 -        |> Thm.adjust_maxidx_thm);
     1.8 +        |> Thm.adjust_maxidx_thm ~1);
     1.9    in (ths, cache') end;
    1.10  
    1.11  end;
     2.1 --- a/src/Pure/conjunction.ML	Sun Jul 30 21:28:51 2006 +0200
     2.2 +++ b/src/Pure/conjunction.ML	Sun Jul 30 21:28:52 2006 +0200
     2.3 @@ -139,7 +139,7 @@
     2.4  val B = Free ("B", propT);
     2.5  
     2.6  fun comp_rule th rule =
     2.7 -  Thm.adjust_maxidx_thm (th COMP
     2.8 +  Thm.adjust_maxidx_thm ~1 (th COMP
     2.9      (rule |> Drule.forall_intr_frees |> Drule.forall_elim_vars (Thm.maxidx_of th + 1)));
    2.10  
    2.11  in
     3.1 --- a/src/Pure/drule.ML	Sun Jul 30 21:28:51 2006 +0200
     3.2 +++ b/src/Pure/drule.ML	Sun Jul 30 21:28:52 2006 +0200
     3.3 @@ -416,7 +416,7 @@
     3.4      val (instT, inst) = Term.zero_var_indexes_inst (Thm.full_prop_of th);
     3.5      val cinstT = map (fn (v, T) => (certT (TVar v), certT T)) instT;
     3.6      val cinst = map (fn (v, t) => (cert (Var v), cert t)) inst;
     3.7 -  in Thm.adjust_maxidx_thm (Thm.instantiate (cinstT, cinst) th) end;
     3.8 +  in Thm.adjust_maxidx_thm ~1 (Thm.instantiate (cinstT, cinst) th) end;
     3.9  
    3.10  
    3.11  (** Standard form of object-rule: no hypotheses, flexflex constraints,
     4.1 --- a/src/Pure/goal.ML	Sun Jul 30 21:28:51 2006 +0200
     4.2 +++ b/src/Pure/goal.ML	Sun Jul 30 21:28:52 2006 +0200
     4.3 @@ -153,7 +153,7 @@
     4.4    (if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty
     4.5     else if n = 1 then Seq.single (Thm.cprem_of st i)
     4.6     else Seq.single (foldr1 Conjunction.mk_conjunction (map (Thm.cprem_of st) (i upto i + n - 1))))
     4.7 -  |> Seq.map (Thm.adjust_maxidx #> init);
     4.8 +  |> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init);
     4.9  
    4.10  fun retrofit i n st' st =
    4.11    (if n = 1 then st
     5.1 --- a/src/Pure/meta_simplifier.ML	Sun Jul 30 21:28:51 2006 +0200
     5.2 +++ b/src/Pure/meta_simplifier.ML	Sun Jul 30 21:28:52 2006 +0200
     5.3 @@ -1161,7 +1161,7 @@
     5.4  
     5.5  fun rewrite_cterm mode prover raw_ss raw_ct =
     5.6    let
     5.7 -    val ct = Thm.adjust_maxidx raw_ct;
     5.8 +    val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
     5.9      val {thy, t, maxidx, ...} = Thm.rep_cterm ct;
    5.10      val ss = fallback_context thy raw_ss;
    5.11      val _ = inc simp_depth;
    5.12 @@ -1210,7 +1210,7 @@
    5.13  fun gen_norm_hhf ss =
    5.14    (not o Drule.is_norm_hhf o Thm.prop_of) ?
    5.15      Drule.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) ss)
    5.16 -  #> Thm.adjust_maxidx_thm
    5.17 +  #> Thm.adjust_maxidx_thm ~1
    5.18    #> Drule.gen_all;
    5.19  
    5.20  val ss = theory_context ProtoPure.thy empty_ss addsimps [Drule.norm_hhf_eq];