# HG changeset patch
# User berghofe
# Date 1184147165 -7200
# Node ID 77e796fe89eb197acb620e258c2c237cc2fb225d
# Parent  997e5fe475328be080729ff0e10056f5de5e4034
Adapted to changes in Accessible_Part theory.

diff -r 997e5fe47532 -r 77e796fe89eb src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Wed Jul 11 11:44:51 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Wed Jul 11 11:46:05 2007 +0200
@@ -17,7 +17,7 @@
 fun PROFILE msg = if !profile then timeap_msg msg else I
 
 
-val acc_const_name = "Accessible_Part.acc"
+val acc_const_name = "Accessible_Part.accp"
 fun mk_acc domT R =
     Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 
 
diff -r 997e5fe47532 -r 77e796fe89eb src/HOL/Tools/function_package/fundef_core.ML
--- a/src/HOL/Tools/function_package/fundef_core.ML	Wed Jul 11 11:44:51 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_core.ML	Wed Jul 11 11:46:05 2007 +0200
@@ -94,17 +94,17 @@
 (* Theory dependencies. *)
 val Pair_inject = thm "Product_Type.Pair_inject";
 
-val acc_induct_rule = thm "Accessible_Part.acc_induct_rule"
+val acc_induct_rule = thm "Accessible_Part.accp_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 "Accessible_Part.acc_downward"
-val accI = thm "Accessible_Part.accI"
+val acc_downward = thm "Accessible_Part.accp_downward"
+val accI = thm "Accessible_Part.accp.accI"
 val case_split = thm "HOL.case_split_thm"
 val fundef_default_value = thm "FunDef.fundef_default_value"
-val not_acc_down = thm "Accessible_Part.not_acc_down"
+val not_acc_down = thm "Accessible_Part.not_accp_down"
 
 
 
@@ -573,7 +573,7 @@
 
 
 val acc_subset_induct = thm "Fun.predicate1I" RS
-  thm "Accessible_Part.acc_subset_induct"
+  thm "Accessible_Part.accp_subset_induct"
 
 fun mk_partial_induct_rule thy globals R complete_thm clauses =
     let
@@ -704,8 +704,8 @@
 (** Termination rule **)
 
 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";
+val wf_in_rel = thm "FunDef.wf_in_rel";
+val in_rel_def = thm "FunDef.in_rel_def";
 
 fun mk_nest_term_case thy globals R' ihyp clause =
     let
@@ -768,7 +768,7 @@
       val R' = Free ("R", fastype_of R)
                
       val Rrel = Free ("R", mk_relT (domT, domT))
-      val inrel_R = Const ("Predicate.member2", mk_relT (domT, domT) --> fastype_of R) $ Rrel
+      val inrel_R = Const ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) $ Rrel
                     
       val wfR' = cterm_of thy (Trueprop (Const ("Wellfounded_Recursion.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)