1.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Feb 27 21:41:08 2008 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Feb 27 21:46:13 2008 +0100
     1.3 @@ -297,19 +297,22 @@
     1.4      #> Context.theory_map (FundefCommon.set_preproc sequential_preproc)
     1.5  
     1.6  
     1.7 -val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", 
     1.8 +val fun_config = FundefConfig { sequential=true, default="%x. arbitrary" (* FIXME dynamic scoping *), 
     1.9                                  target=NONE, domintros=false, tailrec=false }
    1.10  
    1.11  
    1.12  local structure P = OuterParse and K = OuterKeyword in
    1.13  
    1.14  fun fun_cmd config fixes statements flags lthy =
    1.15 +  let val group = serial_string () in
    1.16      lthy
    1.17 -      |> LocalTheory.set_group (serial_string ())
    1.18 +      |> LocalTheory.set_group group
    1.19        |> FundefPackage.add_fundef fixes statements config flags
    1.20        |> by_pat_completeness_simp
    1.21        |> LocalTheory.reinit
    1.22 +      |> LocalTheory.set_group group
    1.23        |> termination_by_lexicographic_order
    1.24 +  end;
    1.25  
    1.26  val _ =
    1.27    OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl

     2.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Feb 27 21:41:08 2008 +0100
     2.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Feb 27 21:46:13 2008 +0100
     2.3 @@ -150,6 +150,10 @@
     2.4          |> Proof.theorem_i NONE (total_termination_afterqed data) [[(goal, [])]]
     2.5      end
     2.6  
     2.7 +fun termination_cmd term_opt lthy =
     2.8 +  lthy
     2.9 +  |> LocalTheory.set_group (serial_string ())
    2.10 +  |> setup_termination_proof term_opt;
    2.11  
    2.12  val add_fundef = gen_add_fundef true Specification.read_specification
    2.13  val add_fundef_i = gen_add_fundef false Specification.check_specification
    2.14 @@ -272,7 +276,7 @@
    2.15    (P.opt_target -- Scan.option P.term
    2.16      >> (fn (target, name) =>
    2.17             Toplevel.print o
    2.18 -           Toplevel.local_theory_to_proof target (setup_termination_proof name)));
    2.19 +           Toplevel.local_theory_to_proof target (termination_cmd name)));
    2.20  
    2.21  end;
    2.22