# HG changeset patch
# User wenzelm
# Date 1122556799 -7200
# Node ID c01816b32c045e1c5fe0011422a0501eff6181c0
# Parent  0bda949449ee9bcd26de22cd5a9eb376bae38343
norm_hhf_rule: Thm.adjust_maxidx_thm before Drule.gen_all;
removed prove_standard, prove_multi_standard;

diff -r 0bda949449ee -r c01816b32c04 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Thu Jul 28 15:19:58 2005 +0200
+++ b/src/Pure/tactic.ML	Thu Jul 28 15:19:59 2005 +0200
@@ -116,12 +116,8 @@
     (thm list -> tactic) -> thm list
   val prove_multi: theory -> string list -> term list -> term list ->
     (thm list -> tactic) -> thm list
-  val prove_multi_standard: theory -> string list -> term list -> term list ->
-    (thm list -> tactic) -> thm list
   val prove_plain: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
   val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
-  val prove_standard: theory -> string list -> term list -> term ->
-    (thm list -> tactic) -> thm
   val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
                           int -> tactic
   val lift_inst_rule'   : thm * int * (indexname * string) list * thm -> thm
@@ -550,11 +546,13 @@
 fun rewtac def = rewrite_goals_tac [def];
 
 fun norm_hhf_plain th =
-  if Drule.is_norm_hhf (prop_of th) then th
+  if Drule.is_norm_hhf (Thm.prop_of th) then th
   else rewrite_rule [Drule.norm_hhf_eq] th;
 
-fun norm_hhf_rule th =
-  th |> norm_hhf_plain |> Drule.gen_all;
+val norm_hhf_rule =
+  norm_hhf_plain
+  #> Thm.adjust_maxidx_thm
+  #> Drule.gen_all;
 
 val norm_hhf_tac =
   rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
@@ -711,12 +709,9 @@
   gen_prove_multi (fn fixed_tfrees => Drule.zero_var_indexes o
       (#1 o Thm.varifyT' fixed_tfrees) o norm_hhf_rule)
     thy xs asms prop tac;
-fun prove_multi_standard thy xs asms prop tac =
-  map Drule.standard (prove_multi thy xs asms prop tac);
 
 fun prove_plain thy xs asms prop tac = hd (prove_multi_plain thy xs asms [prop] tac);
 fun prove thy xs asms prop tac = hd (prove_multi thy xs asms [prop] tac);
-fun prove_standard thy xs asms prop tac = Drule.standard (prove thy xs asms prop tac);
 
 end;