# HG changeset patch
# User haftmann
# Date 1174077139 -3600
# Node ID 052cfe1c86dc5ff66ebcd5b5bc17eff6895a706c
# Parent  b4f96f343d6cd0786dfb58a51d4fb87b5412fa17
adjusted qualified thm reference

diff -r b4f96f343d6c -r 052cfe1c86dc src/HOL/Tools/function_package/fundef_core.ML
--- a/src/HOL/Tools/function_package/fundef_core.ML	Fri Mar 16 21:32:18 2007 +0100
+++ b/src/HOL/Tools/function_package/fundef_core.ML	Fri Mar 16 21:32:19 2007 +0100
@@ -572,7 +572,7 @@
 (** Induction rule **)
 
 
-val acc_subset_induct = thm "FixedPoint.predicate1I" RS
+val acc_subset_induct = thm "Fun.predicate1I" RS
   thm "Accessible_Part.acc_subset_induct"
 
 fun mk_partial_induct_rule thy globals R complete_thm clauses =