src/HOL/Tools/function_package/fundef_package.ML
changeset 26171 5426a823455c
parent 26129 14f6dbb195c4
child 26529 03ad378ed5f0
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Feb 27 21:41:08 2008 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Feb 27 21:46:13 2008 +0100
     1.3 @@ -150,6 +150,10 @@
     1.4          |> Proof.theorem_i NONE (total_termination_afterqed data) [[(goal, [])]]
     1.5      end
     1.6  
     1.7 +fun termination_cmd term_opt lthy =
     1.8 +  lthy
     1.9 +  |> LocalTheory.set_group (serial_string ())
    1.10 +  |> setup_termination_proof term_opt;
    1.11  
    1.12  val add_fundef = gen_add_fundef true Specification.read_specification
    1.13  val add_fundef_i = gen_add_fundef false Specification.check_specification
    1.14 @@ -272,7 +276,7 @@
    1.15    (P.opt_target -- Scan.option P.term
    1.16      >> (fn (target, name) =>
    1.17             Toplevel.print o
    1.18 -           Toplevel.local_theory_to_proof target (setup_termination_proof name)));
    1.19 +           Toplevel.local_theory_to_proof target (termination_cmd name)));
    1.20  
    1.21  end;
    1.22