# HG changeset patch
# User wenzelm
# Date 1211659495 -7200
# Node ID 9b2acb536228c55cb35b2ebb05c5a366ef14f529
# Parent  742e262132129bc225058dca9e11dd0bd409af2c
uniform treatment of target, not as config;

diff -r 742e26213212 -r 9b2acb536228 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Sat May 24 22:04:52 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Sat May 24 22:04:55 2008 +0200
@@ -119,7 +119,8 @@
 
 val all_fundef_data = NetRules.rules o FundefData.get
 
-structure TerminationSimps = NamedThmsFun(
+structure TerminationSimps = NamedThmsFun
+(
   val name = "termination_simp" 
   val description = "Simplification rule for termination proofs"
 );
@@ -144,7 +145,6 @@
 datatype fundef_opt 
   = Sequential
   | Default of string
-  | Target of xstring
   | DomIntros
   | Tailrec
 
@@ -153,26 +153,21 @@
    {
     sequential: bool,
     default: string,
-    target: xstring option,
     domintros: bool,
     tailrec: bool
    }
 
-fun apply_opt Sequential (FundefConfig {sequential, default, target, domintros,tailrec}) = 
-    FundefConfig {sequential=true, default=default, target=target, domintros=domintros, tailrec=tailrec}
-  | apply_opt (Default d) (FundefConfig {sequential, default, target, domintros,tailrec}) = 
-    FundefConfig {sequential=sequential, default=d, target=target, domintros=domintros, tailrec=tailrec}
-  | apply_opt (Target t) (FundefConfig {sequential, default, target, domintros,tailrec}) =
-    FundefConfig {sequential=sequential, default=default, target=SOME t, domintros=domintros, tailrec=tailrec}
-  | apply_opt DomIntros (FundefConfig {sequential, default, target, domintros,tailrec}) =
-    FundefConfig {sequential=sequential, default=default, target=target, domintros=true,tailrec=tailrec}
-  | apply_opt Tailrec (FundefConfig {sequential, default, target, domintros,tailrec}) =
-    FundefConfig {sequential=sequential, default=default, target=target, domintros=domintros,tailrec=true}
+fun apply_opt Sequential (FundefConfig {sequential, default, domintros,tailrec}) = 
+    FundefConfig {sequential=true, default=default, domintros=domintros, tailrec=tailrec}
+  | apply_opt (Default d) (FundefConfig {sequential, default, domintros,tailrec}) = 
+    FundefConfig {sequential=sequential, default=d, domintros=domintros, tailrec=tailrec}
+  | apply_opt DomIntros (FundefConfig {sequential, default, domintros,tailrec}) =
+    FundefConfig {sequential=sequential, default=default, domintros=true,tailrec=tailrec}
+  | apply_opt Tailrec (FundefConfig {sequential, default, domintros,tailrec}) =
+    FundefConfig {sequential=sequential, default=default, domintros=domintros,tailrec=true}
 
-fun target_of (FundefConfig {target, ...}) = target
-
-val default_config = FundefConfig { sequential=false, default="%x. arbitrary", 
-                                    target=NONE, domintros=false, tailrec=false }
+val default_config =
+  FundefConfig { sequential=false, default="%x. arbitrary", domintros=false, tailrec=false }
 
 
 (* Common operations on equations *)
@@ -311,7 +306,6 @@
                    || ((P.reserved "default" |-- P.term) >> Default)
                    || (P.reserved "domintros" >> K DomIntros)
                    || (P.reserved "tailrec" >> K Tailrec)
-                   || ((P.$$$ "in" |-- P.xname) >> Target)
 
   fun config_parser default = (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 (P.group "option" option_parser)) --| P.$$$ ")") [])
                               >> (fn opts => fold apply_opt opts default)
diff -r 742e26213212 -r 9b2acb536228 src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Sat May 24 22:04:52 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Sat May 24 22:04:55 2008 +0200
@@ -298,7 +298,7 @@
 
 
 val fun_config = FundefConfig { sequential=true, default="%x. arbitrary" (* FIXME dynamic scoping *), 
-                                target=NONE, domintros=false, tailrec=false }
+                                domintros=false, tailrec=false }
 
 
 local structure P = OuterParse and K = OuterKeyword in
@@ -315,10 +315,9 @@
   end;
 
 val _ =
-  OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl
+  OuterSyntax.local_theory "fun" "define general recursive functions (short version)" K.thy_decl
   (fundef_parser fun_config
-     >> (fn ((config, fixes), (flags, statements)) =>
-            (Toplevel.local_theory (target_of config) (fun_cmd config fixes statements flags))));
+     >> (fn ((config, fixes), (flags, statements)) => fun_cmd config fixes statements flags));
 
 end
 
diff -r 742e26213212 -r 9b2acb536228 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Sat May 24 22:04:52 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Sat May 24 22:04:55 2008 +0200
@@ -196,18 +196,13 @@
 val _ = OuterSyntax.keywords ["otherwise"];
 
 val _ =
-  OuterSyntax.command "function" "define general recursive functions" K.thy_goal
+  OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
   (fundef_parser default_config
-     >> (fn ((config, fixes), (flags, statements)) =>
-            Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config flags)
-            #> Toplevel.print));
+     >> (fn ((config, fixes), (flags, statements)) => add_fundef fixes statements config flags));
 
 val _ =
-  OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
-  (P.opt_target -- Scan.option P.term
-    >> (fn (target, name) =>
-           Toplevel.print o
-           Toplevel.local_theory_to_proof target (termination_cmd name)));
+  OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal
+  (Scan.option P.term >> termination_cmd);
 
 end;