# HG changeset patch # User wenzelm # Date 1154287732 -7200 # Node ID 990dbc007ca6bea09c220463ff6477fdc3e5812d # Parent 5eda3b38ec9073cb993885861fe899316104c9dc Thm.adjust_maxidx; diff -r 5eda3b38ec90 -r 990dbc007ca6 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Sun Jul 30 21:28:51 2006 +0200 +++ b/src/Pure/axclass.ML Sun Jul 30 21:28:52 2006 +0200 @@ -425,7 +425,7 @@ sort |> map (fn c => Goal.finish (the (lookup_type cache' typ c) RS Goal.init (Thm.cterm_of thy (Logic.mk_inclass (typ, c)))) - |> Thm.adjust_maxidx_thm); + |> Thm.adjust_maxidx_thm ~1); in (ths, cache') end; end; diff -r 5eda3b38ec90 -r 990dbc007ca6 src/Pure/conjunction.ML --- a/src/Pure/conjunction.ML Sun Jul 30 21:28:51 2006 +0200 +++ b/src/Pure/conjunction.ML Sun Jul 30 21:28:52 2006 +0200 @@ -139,7 +139,7 @@ val B = Free ("B", propT); fun comp_rule th rule = - Thm.adjust_maxidx_thm (th COMP + Thm.adjust_maxidx_thm ~1 (th COMP (rule |> Drule.forall_intr_frees |> Drule.forall_elim_vars (Thm.maxidx_of th + 1))); in diff -r 5eda3b38ec90 -r 990dbc007ca6 src/Pure/drule.ML --- a/src/Pure/drule.ML Sun Jul 30 21:28:51 2006 +0200 +++ b/src/Pure/drule.ML Sun Jul 30 21:28:52 2006 +0200 @@ -416,7 +416,7 @@ val (instT, inst) = Term.zero_var_indexes_inst (Thm.full_prop_of th); val cinstT = map (fn (v, T) => (certT (TVar v), certT T)) instT; val cinst = map (fn (v, t) => (cert (Var v), cert t)) inst; - in Thm.adjust_maxidx_thm (Thm.instantiate (cinstT, cinst) th) end; + in Thm.adjust_maxidx_thm ~1 (Thm.instantiate (cinstT, cinst) th) end; (** Standard form of object-rule: no hypotheses, flexflex constraints, diff -r 5eda3b38ec90 -r 990dbc007ca6 src/Pure/goal.ML --- a/src/Pure/goal.ML Sun Jul 30 21:28:51 2006 +0200 +++ b/src/Pure/goal.ML Sun Jul 30 21:28:52 2006 +0200 @@ -153,7 +153,7 @@ (if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty else if n = 1 then Seq.single (Thm.cprem_of st i) else Seq.single (foldr1 Conjunction.mk_conjunction (map (Thm.cprem_of st) (i upto i + n - 1)))) - |> Seq.map (Thm.adjust_maxidx #> init); + |> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init); fun retrofit i n st' st = (if n = 1 then st diff -r 5eda3b38ec90 -r 990dbc007ca6 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Sun Jul 30 21:28:51 2006 +0200 +++ b/src/Pure/meta_simplifier.ML Sun Jul 30 21:28:52 2006 +0200 @@ -1161,7 +1161,7 @@ fun rewrite_cterm mode prover raw_ss raw_ct = let - val ct = Thm.adjust_maxidx raw_ct; + val ct = Thm.adjust_maxidx_cterm ~1 raw_ct; val {thy, t, maxidx, ...} = Thm.rep_cterm ct; val ss = fallback_context thy raw_ss; val _ = inc simp_depth; @@ -1210,7 +1210,7 @@ fun gen_norm_hhf ss = (not o Drule.is_norm_hhf o Thm.prop_of) ? Drule.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) ss) - #> Thm.adjust_maxidx_thm + #> Thm.adjust_maxidx_thm ~1 #> Drule.gen_all; val ss = theory_context ProtoPure.thy empty_ss addsimps [Drule.norm_hhf_eq];