src/HOL/Tools/function_package/fundef_package.ML
changeset 21211 5370cfbf3070
parent 21051 c49467a9c1e1
child 21235 674e2731b519
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Nov 07 11:47:57 2006 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Nov 07 11:53:55 2006 +0100
     1.3 @@ -13,13 +13,15 @@
     1.4                        -> ((bstring * Attrib.src list) * string list) list list
     1.5                        -> FundefCommon.fundef_config
     1.6                        -> local_theory
     1.7 -                      -> Proof.state
     1.8 +                      -> string * Proof.state
     1.9  
    1.10      val add_fundef_i:  (string * typ option * mixfix) list
    1.11                         -> ((bstring * Attrib.src list) * term list) list list
    1.12                         -> bool
    1.13                         -> local_theory
    1.14 -                       -> Proof.state
    1.15 +                       -> string * Proof.state
    1.16 +
    1.17 +    val setup_termination_proof : string option -> local_theory -> Proof.state
    1.18  
    1.19      val cong_add: attribute
    1.20      val cong_del: attribute
    1.21 @@ -105,9 +107,9 @@
    1.22  
    1.23        val afterqed = fundef_afterqed fixes spec mutual_info name prep_result
    1.24      in
    1.25 -        lthy
    1.26 -          |> Proof.theorem_i PureThy.internalK NONE afterqed NONE ("", []) [(("", []), [(goal, [])])]
    1.27 -          |> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd
    1.28 +      (name, lthy
    1.29 +         |> Proof.theorem_i PureThy.internalK NONE afterqed NONE ("", []) [(("", []), [(goal, [])])]
    1.30 +         |> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd)
    1.31      end
    1.32  
    1.33  
    1.34 @@ -132,7 +134,7 @@
    1.35      end
    1.36  
    1.37  
    1.38 -fun fundef_setup_termination_proof name_opt lthy =
    1.39 +fun setup_termination_proof name_opt lthy =
    1.40      let
    1.41          val name = the_default (get_last_fundef (Context.Proof lthy)) name_opt
    1.42          val data = the (get_fundef_data name (Context.Proof lthy))
    1.43 @@ -190,8 +192,8 @@
    1.44    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
    1.45    ((config_parser default_config -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
    1.46       >> (fn (((config, target), fixes), statements) =>
    1.47 -            Toplevel.print o
    1.48 -            Toplevel.local_theory_to_proof target (add_fundef fixes statements config)));
    1.49 +            Toplevel.local_theory_to_proof target (add_fundef fixes statements config #> snd)
    1.50 +            #> Toplevel.print));
    1.51  
    1.52  
    1.53  
    1.54 @@ -200,7 +202,7 @@
    1.55    (P.opt_locale_target -- Scan.option P.name
    1.56      >> (fn (target, name) =>
    1.57             Toplevel.print o
    1.58 -           Toplevel.local_theory_to_proof target (fundef_setup_termination_proof name)));
    1.59 +           Toplevel.local_theory_to_proof target (setup_termination_proof name)));
    1.60  
    1.61  
    1.62  val _ = OuterSyntax.add_parsers [functionP];