# HG changeset patch
# User berghofe
# Date 1170867798 -3600
# Node ID b0d482a9443fd6908cc93db3b60e02f29d9e95a3
# Parent  70a7cd02fec148e6a5be1c0a70e436cd0b49ccd5
Adapted to changes in Accessible_Part and Wellfounded_Recursion theories.

diff -r 70a7cd02fec1 -r b0d482a9443f src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Wed Feb 07 18:01:40 2007 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Wed Feb 07 18:03:18 2007 +0100
@@ -10,7 +10,7 @@
 struct
 
 (* Theory Dependencies *)
-val acc_const_name = "FunDef.accP"
+val acc_const_name = "Accessible_Part.acc"
 
 val profile = ref false;
 
diff -r 70a7cd02fec1 -r b0d482a9443f src/HOL/Tools/function_package/fundef_core.ML
--- a/src/HOL/Tools/function_package/fundef_core.ML	Wed Feb 07 18:01:40 2007 +0100
+++ b/src/HOL/Tools/function_package/fundef_core.ML	Wed Feb 07 18:03:18 2007 +0100
@@ -95,17 +95,17 @@
 (* Theory dependencies. *)
 val Pair_inject = thm "Product_Type.Pair_inject";
 
-val acc_induct_rule = thm "FunDef.accP_induct_rule"
+val acc_induct_rule = thm "Accessible_Part.acc_induct_rule"
 
 val ex1_implies_ex = thm "FunDef.fundef_ex1_existence"
 val ex1_implies_un = thm "FunDef.fundef_ex1_uniqueness"
 val ex1_implies_iff = thm "FunDef.fundef_ex1_iff"
 
-val acc_downward = thm "FunDef.accP_downward"
-val accI = thm "FunDef.accPI"
+val acc_downward = thm "Accessible_Part.acc_downward"
+val accI = thm "Accessible_Part.accI"
 val case_split = thm "HOL.case_split_thm"
 val fundef_default_value = thm "FunDef.fundef_default_value"
-val not_accP_down = thm "FunDef.not_accP_down"
+val not_acc_down = thm "Accessible_Part.not_acc_down"
 
 
 
@@ -572,7 +572,8 @@
 (** Induction rule **)
 
 
-val acc_subset_induct = thm "FunDef.accP_subset_induct"
+val acc_subset_induct = thm "FixedPoint.predicate1I" RS
+  thm "Accessible_Part.acc_subset_induct"
 
 fun mk_partial_induct_rule thy globals R complete_thm clauses =
     let
@@ -702,9 +703,9 @@
 
 (** Termination rule **)
 
-val wf_induct_rule = thm "FunDef.wfP_induct_rule";
-val wf_in_rel = thm "FunDef.wf_in_rel";
-val in_rel_def = thm "FunDef.in_rel_def";
+val wf_induct_rule = thm "Wellfounded_Recursion.wfP_induct_rule";
+val wf_in_rel = thm "Wellfounded_Recursion.wf_implies_wfP";
+val in_rel_def = thm "Predicate.member2_eq";
 
 fun mk_nest_term_case thy globals R' ihyp clause =
     let
@@ -767,9 +768,9 @@
       val R' = Free ("R", fastype_of R)
                
       val Rrel = Free ("R", mk_relT (domT, domT))
-      val inrel_R = Const ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) $ Rrel
+      val inrel_R = Const ("Predicate.member2", mk_relT (domT, domT) --> fastype_of R) $ Rrel
                     
-      val wfR' = cterm_of thy (Trueprop (Const ("FunDef.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
+      val wfR' = cterm_of thy (Trueprop (Const ("Wellfounded_Recursion.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
                           
       (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
       val ihyp = all domT $ Abs ("z", domT, 
@@ -845,7 +846,7 @@
                            rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
                                 THEN (rtac (forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
                                 THEN (SIMPSET (fn ss => asm_full_simp_tac (ss addsimps [default_thm]) 1))
-                                THEN (etac not_accP_down 1)
+                                THEN (etac not_acc_down 1)
                                 THEN ((etac R_cases) THEN_ALL_NEW (SIMPSET' (fn ss => asm_full_simp_tac (ss addsimps [default_thm])))) 1)
               |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
           end