# HG changeset patch
# User wenzelm
# Date 1160177463 -7200
# Node ID 95d24e8d117e90396149dbff1989af348e3972bd
# Parent  1316db4819440f78de5c3466b4ebe202f5c422b1
TheoryTarget.init;

diff -r 1316db481944 -r 95d24e8d117e src/HOL/Tools/function_package/fundef_datatype.ML
--- 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