# HG changeset patch
# User wenzelm
# Date 1130531267 -7200
# Node ID 3900037edf3d94be26b5479a5e8b50fab61e1688
# Parent  c1bb6480534f77f327c079a5a2dd43449754f791
accomodate simplified Thm.lift_rule;

diff -r c1bb6480534f -r 3900037edf3d src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Fri Oct 28 22:27:46 2005 +0200
+++ b/src/HOL/Tools/record_package.ML	Fri Oct 28 22:27:47 2005 +0200
@@ -1234,7 +1234,7 @@
     val g = nth (prems_of st) (i - 1);
     val params = Logic.strip_params g;
     val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
-    val rule' = Thm.lift_rule (st, i) rule;
+    val rule' = Thm.lift_rule (Thm.cgoal_of st i) rule;
     val (P, ys) = strip_comb (HOLogic.dest_Trueprop
       (Logic.strip_assums_concl (prop_of rule')));
     (* ca indicates if rule is a case analysis or induction rule *)
@@ -1260,7 +1260,7 @@
     val sg = sign_of_thm st;
     val g = nth (prems_of st) (i - 1);
     val params = Logic.strip_params g;
-    val exI' = Thm.lift_rule (st, i) exI;
+    val exI' = Thm.lift_rule (Thm.cgoal_of st i) exI;
     val (_$(_$x)) = Logic.strip_assums_concl (hd (prems_of exI'));
     val cx = cterm_of sg (fst (strip_comb x));
 
diff -r c1bb6480534f -r 3900037edf3d src/HOLCF/adm_tac.ML
--- a/src/HOLCF/adm_tac.ML	Fri Oct 28 22:27:46 2005 +0200
+++ b/src/HOLCF/adm_tac.ML	Fri Oct 28 22:27:47 2005 +0200
@@ -113,7 +113,7 @@
   let val {sign, maxidx, ...} = rep_thm state;
       val j = maxidx+1;
       val parTs = map snd (rev params);
-      val rule = lift_rule (state, i) adm_subst;
+      val rule = Thm.lift_rule (Thm.cgoal_of state i) adm_subst;
       val types = valOf o (fst (types_sorts rule));
       val tT = types ("t", j);
       val PT = types ("P", j);
diff -r c1bb6480534f -r 3900037edf3d src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Fri Oct 28 22:27:46 2005 +0200
+++ b/src/Provers/induct_method.ML	Fri Oct 28 22:27:47 2005 +0200
@@ -157,7 +157,7 @@
   Tactic.rewrite_goal_tac Data.rulify2 THEN'
   Tactic.norm_hhf_tac;
 
-val localize = Goal.norm_hhf_rule o Tactic.simplify false Data.localize;
+val localize = Goal.norm_hhf o Tactic.simplify false Data.localize;
 
 
 (* imp_intr --- limited to atomic prems *)
@@ -168,8 +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 = Goal.init (Drule.list_implies (As, C));
-  in th COMP Thm.lift_rule (dummy_st, 1) Data.local_impI end;
+  in th COMP Thm.lift_rule (Drule.list_implies (As, C)) Data.local_impI end;
 
 
 (* join multi-rules *)
diff -r c1bb6480534f -r 3900037edf3d src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Fri Oct 28 22:27:46 2005 +0200
+++ b/src/Provers/splitter.ML	Fri Oct 28 22:27:47 2005 +0200
@@ -302,7 +302,7 @@
 
 fun inst_split Ts t tt thm TB state i =
   let
-    val thm' = Thm.lift_rule (state, i) thm;
+    val thm' = Thm.lift_rule (Thm.cgoal_of state i) thm;
     val (P, _) = strip_comb (fst (Logic.dest_equals
       (Logic.strip_assums_concl (#prop (rep_thm thm')))));
     val cert = cterm_of (sign_of_thm state);