MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
authorwenzelm
Thu Jan 17 21:01:17 2002 +0100 (2002-01-17 ago)
changeset 12798f7e2d0d32ea7
parent 12797 4de06a8f67ef
child 12799 5472afdd3bd3
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Jan 17 21:00:38 2002 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Jan 17 21:01:17 2002 +0100
     1.3 @@ -296,7 +296,7 @@
     1.4  val all_not_allowed = 
     1.5      "Introduction rule must not have a leading \"!!\" quantifier";
     1.6  
     1.7 -val atomize_cterm = Tactic.rewrite_cterm true inductive_atomize;
     1.8 +fun atomize_term sg = MetaSimplifier.rewrite_term sg inductive_atomize;
     1.9  
    1.10  in
    1.11  
    1.12 @@ -304,7 +304,7 @@
    1.13    let
    1.14      val concl = Logic.strip_imp_concl rule;
    1.15      val prems = Logic.strip_imp_prems rule;
    1.16 -    val aprems = prems |> map (Thm.term_of o atomize_cterm o Thm.cterm_of sg);
    1.17 +    val aprems = map (atomize_term sg) prems;
    1.18      val arule = Logic.list_implies (aprems, concl);
    1.19  
    1.20      fun check_prem (prem, aprem) =
    1.21 @@ -324,7 +324,7 @@
    1.22    end;
    1.23  
    1.24  val rulify =
    1.25 -  standard o Tactic.norm_hhf o
    1.26 +  standard o Tactic.norm_hhf_rule o
    1.27    hol_simplify inductive_rulify2 o hol_simplify inductive_rulify1 o
    1.28    hol_simplify inductive_conj;
    1.29