Tactic.rewrite_cterm;
authorwenzelm
Mon Oct 15 20:35:10 2001 +0200 (2001-10-15)
changeset 11781a08b62908caa
parent 11780 d17ee2241257
child 11782 bdd2ac7c75ff
Tactic.rewrite_cterm;
src/HOL/Tools/inductive_package.ML
src/Provers/induct_method.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Oct 15 20:34:44 2001 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Oct 15 20:35:10 2001 +0200
     1.3 @@ -295,7 +295,7 @@
     1.4  val all_not_allowed = 
     1.5      "Introduction rule must not have a leading \"!!\" quantifier";
     1.6  
     1.7 -val atomize_cterm = rewrite_cterm true inductive_atomize;
     1.8 +val atomize_cterm = Tactic.rewrite_cterm true inductive_atomize;
     1.9  
    1.10  in
    1.11  
     2.1 --- a/src/Provers/induct_method.ML	Mon Oct 15 20:34:44 2001 +0200
     2.2 +++ b/src/Provers/induct_method.ML	Mon Oct 15 20:35:10 2001 +0200
     2.3 @@ -147,11 +147,11 @@
     2.4  local
     2.5  
     2.6  fun atomize_cterm ct =
     2.7 -  Thm.cterm_fun
     2.8 -    (ObjectLogic.drop_judgment (#sign (Thm.rep_cterm ct))) (rewrite_cterm true Data.atomize ct);
     2.9 +  Thm.cterm_fun (ObjectLogic.drop_judgment (#sign (Thm.rep_cterm ct)))
    2.10 +    (Tactic.rewrite_cterm true Data.atomize ct);
    2.11  
    2.12  val atomize_tac = Tactic.rewrite_goal_tac Data.atomize;
    2.13 -val rulify_cterm = rewrite_cterm true Data.rulify2 o rewrite_cterm true Data.rulify1;
    2.14 +val rulify_cterm = Tactic.rewrite_cterm true Data.rulify2 o Tactic.rewrite_cterm true Data.rulify1;
    2.15  
    2.16  val rulify_tac =
    2.17    Tactic.rewrite_goal_tac Data.rulify1 THEN'