TheoryTarget.init;

--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Sat Oct 07 01:31:02 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Sat Oct 07 01:31:03 2006 +0200
@@ -181,7 +181,7 @@
 
 
 fun local_theory_to_proof f = 
-    Toplevel.theory_to_proof (f o LocalTheory.init NONE)
+    Toplevel.theory_to_proof (f o TheoryTarget.init NONE)
 
 fun or_list1 s = P.enum1 "|" s
 val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
@@ -205,4 +205,4 @@
 
 
 
-end
\ No newline at end of file
+end