src/Pure/goal.ML
changeset 23536 60a1672e298e
parent 23418 c195f6f13769
child 25301 24e027f55f45
     1.1 --- a/src/Pure/goal.ML	Tue Jul 03 17:17:09 2007 +0200
     1.2 +++ b/src/Pure/goal.ML	Tue Jul 03 17:17:11 2007 +0200
     1.3 @@ -32,8 +32,6 @@
     1.4    val conjunction_tac: int -> tactic
     1.5    val precise_conjunction_tac: int -> int -> tactic
     1.6    val recover_conjunction_tac: tactic
     1.7 -  val asm_rewrite_goal_tac: bool * bool * bool -> (simpset -> tactic) -> simpset -> int -> tactic
     1.8 -  val rewrite_goal_tac: thm list -> int -> tactic
     1.9    val norm_hhf_tac: int -> tactic
    1.10    val compose_hhf: thm -> int -> thm -> thm Seq.seq
    1.11    val compose_hhf_tac: thm -> int -> tactic
    1.12 @@ -209,27 +207,13 @@
    1.13      THEN recover_conjunction_tac);
    1.14  
    1.15  
    1.16 -(* rewriting *)
    1.17 -
    1.18 -(*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
    1.19 -fun asm_rewrite_goal_tac mode prover_tac ss =
    1.20 -  SELECT_GOAL
    1.21 -    (PRIMITIVE (MetaSimplifier.rewrite_goal_rule mode (SINGLE o prover_tac) ss 1));
    1.22 -
    1.23 -fun rewrite_goal_tac rews =
    1.24 -  let val ss = MetaSimplifier.empty_ss addsimps rews in
    1.25 -    fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
    1.26 -      (MetaSimplifier.theory_context (Thm.theory_of_thm st) ss) i st
    1.27 -  end;
    1.28 -
    1.29 -
    1.30  (* hhf normal form *)
    1.31  
    1.32  val norm_hhf_tac =
    1.33    rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
    1.34    THEN' SUBGOAL (fn (t, i) =>
    1.35      if Drule.is_norm_hhf t then all_tac
    1.36 -    else rewrite_goal_tac [Drule.norm_hhf_eq] i);
    1.37 +    else MetaSimplifier.rewrite_goal_tac [Drule.norm_hhf_eq] i);
    1.38  
    1.39  fun compose_hhf tha i thb =
    1.40    Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of thb i) tha, 0) i thb;