# HG changeset patch
# User wenzelm
# Date 1129911281 -7200
# Node ID 6ebd59acf58a57a64914343fd0fb14fde44a3ee2
# Parent  5662fa033a9252529e9f87a9b75096a36c314371
Goal.norm_hhf_rule, Goal.init;

diff -r 5662fa033a92 -r 6ebd59acf58a src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Fri Oct 21 18:14:40 2005 +0200
+++ b/src/Provers/induct_method.ML	Fri Oct 21 18:14:41 2005 +0200
@@ -157,7 +157,7 @@
   Tactic.rewrite_goal_tac Data.rulify2 THEN'
   Tactic.norm_hhf_tac;
 
-val localize = Tactic.norm_hhf_rule o Tactic.simplify false Data.localize;
+val localize = Goal.norm_hhf_rule o Tactic.simplify false Data.localize;
 
 
 (* imp_intr --- limited to atomic prems *)
@@ -168,7 +168,7 @@
     val cprems = Drule.cprems_of th;
     val As = Library.take (length cprems - 1, cprems);
     val C = Thm.cterm_of (Thm.sign_of_thm th) (Var (("C", #maxidx (Thm.rep_thm th) + 1), propT));
-    val dummy_st = Drule.mk_triv_goal (Drule.list_implies (As, C));
+    val dummy_st = Goal.init (Drule.list_implies (As, C));
   in th COMP Thm.lift_rule (dummy_st, 1) Data.local_impI end;