# HG changeset patch
# User wenzelm
# Date 1160686640 -7200
# Node ID 54c42dfbcafa29802820c840f495476cff4b81cc
# Parent  9131d8e96dba0555117bcac3d627de5e0602b5d9
Toplevel.local_theory_to_proof: proper target;

diff -r 9131d8e96dba -r 54c42dfbcafa src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Oct 12 22:57:15 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Oct 12 22:57:20 2006 +0200
@@ -185,20 +185,20 @@
 val statements_ow = or_list1 statement_ow
 
 
-fun local_theory_to_proof f =
-    Toplevel.theory_to_proof (f o TheoryTarget.init NONE)
-
 val functionP =
   OuterSyntax.command "function" "define general recursive functions" K.thy_goal
   ((config_parser -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
      >> (fn (((config, target), fixes), statements) =>
-            Toplevel.print o local_theory_to_proof (add_fundef fixes statements config)));
+            Toplevel.print o
+            Toplevel.local_theory_to_proof target (add_fundef fixes statements config)));
 
 
 val terminationP =
   OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
-  (Scan.option P.name
-    >> (fn name => Toplevel.print o local_theory_to_proof (fundef_setup_termination_proof name)));
+  (P.opt_locale_target -- Scan.option P.name
+    >> (fn (target, name) =>
+           Toplevel.print o
+           Toplevel.local_theory_to_proof target (fundef_setup_termination_proof name)));
 
 
 val _ = OuterSyntax.add_parsers [functionP];