use hol_rewrite_cterm;
authorwenzelm
Fri Feb 02 22:19:52 2001 +0100 (2001-02-02)
changeset 11035bad7568e76e0
parent 11034 568eb11f8d52
child 11036 3c30f7b97a50
use hol_rewrite_cterm;
src/HOL/Tools/induct_method.ML
     1.1 --- a/src/HOL/Tools/induct_method.ML	Fri Feb 02 22:19:23 2001 +0100
     1.2 +++ b/src/HOL/Tools/induct_method.ML	Fri Feb 02 22:19:52 2001 +0100
     1.3 @@ -10,7 +10,6 @@
     1.4  sig
     1.5    val vars_of: term -> term list
     1.6    val concls_of: thm -> term list
     1.7 -  val rewrite_cterm: thm list -> cterm -> cterm
     1.8    val simp_case_tac: bool -> simpset -> int -> tactic
     1.9    val setup: (theory -> theory) list
    1.10  end;
    1.11 @@ -74,8 +73,6 @@
    1.12      |> mapfilter prep_var
    1.13    end;
    1.14  
    1.15 -fun rewrite_cterm rews =
    1.16 -  #2 o Thm.dest_comb o #prop o Thm.crep_thm o Simplifier.full_rewrite (HOL_basic_ss addsimps rews);
    1.17  
    1.18  
    1.19  (* simplifying cases rules *)
    1.20 @@ -206,9 +203,9 @@
    1.21  
    1.22  local
    1.23  
    1.24 -val atomize_cterm = Thm.cterm_fun AutoBind.drop_judgment o rewrite_cterm inductive_atomize;
    1.25 +val atomize_cterm = Thm.cterm_fun AutoBind.drop_judgment o hol_rewrite_cterm inductive_atomize;
    1.26  val atomize_tac = Tactic.rewrite_goal_tac inductive_atomize;
    1.27 -val rulify_cterm = rewrite_cterm inductive_rulify2 o rewrite_cterm inductive_rulify1;
    1.28 +val rulify_cterm = hol_rewrite_cterm inductive_rulify2 o hol_rewrite_cterm inductive_rulify1;
    1.29  
    1.30  val rulify_tac =
    1.31    Tactic.rewrite_goal_tac inductive_rulify1 THEN'