src/Pure/tactic.ML
changeset 16942 c01816b32c04
parent 16876 f57b38cced32
child 17203 29b2563f5c11
     1.1 --- a/src/Pure/tactic.ML	Thu Jul 28 15:19:58 2005 +0200
     1.2 +++ b/src/Pure/tactic.ML	Thu Jul 28 15:19:59 2005 +0200
     1.3 @@ -116,12 +116,8 @@
     1.4      (thm list -> tactic) -> thm list
     1.5    val prove_multi: theory -> string list -> term list -> term list ->
     1.6      (thm list -> tactic) -> thm list
     1.7 -  val prove_multi_standard: theory -> string list -> term list -> term list ->
     1.8 -    (thm list -> tactic) -> thm list
     1.9    val prove_plain: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.10    val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.11 -  val prove_standard: theory -> string list -> term list -> term ->
    1.12 -    (thm list -> tactic) -> thm
    1.13    val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
    1.14                            int -> tactic
    1.15    val lift_inst_rule'   : thm * int * (indexname * string) list * thm -> thm
    1.16 @@ -550,11 +546,13 @@
    1.17  fun rewtac def = rewrite_goals_tac [def];
    1.18  
    1.19  fun norm_hhf_plain th =
    1.20 -  if Drule.is_norm_hhf (prop_of th) then th
    1.21 +  if Drule.is_norm_hhf (Thm.prop_of th) then th
    1.22    else rewrite_rule [Drule.norm_hhf_eq] th;
    1.23  
    1.24 -fun norm_hhf_rule th =
    1.25 -  th |> norm_hhf_plain |> Drule.gen_all;
    1.26 +val norm_hhf_rule =
    1.27 +  norm_hhf_plain
    1.28 +  #> Thm.adjust_maxidx_thm
    1.29 +  #> Drule.gen_all;
    1.30  
    1.31  val norm_hhf_tac =
    1.32    rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
    1.33 @@ -711,12 +709,9 @@
    1.34    gen_prove_multi (fn fixed_tfrees => Drule.zero_var_indexes o
    1.35        (#1 o Thm.varifyT' fixed_tfrees) o norm_hhf_rule)
    1.36      thy xs asms prop tac;
    1.37 -fun prove_multi_standard thy xs asms prop tac =
    1.38 -  map Drule.standard (prove_multi thy xs asms prop tac);
    1.39  
    1.40  fun prove_plain thy xs asms prop tac = hd (prove_multi_plain thy xs asms [prop] tac);
    1.41  fun prove thy xs asms prop tac = hd (prove_multi thy xs asms [prop] tac);
    1.42 -fun prove_standard thy xs asms prop tac = Drule.standard (prove thy xs asms prop tac);
    1.43  
    1.44  end;
    1.45