# HG changeset patch # User wenzelm # Date 1231326622 -3600 # Node ID 9f6e2658a868a2a85559a8a3f96e98a1d488b322 # Parent 45d77aeb16080eea79fb42babb7ab3617c8a2b15 Proof.future_terminal_proof: no fork for interactive mode -- proofs need to be checked immediately here; diff -r 45d77aeb1608 -r 9f6e2658a868 src/HOL/Tools/function_package/fundef_datatype.ML --- a/src/HOL/Tools/function_package/fundef_datatype.ML Wed Jan 07 12:09:39 2009 +0100 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Wed Jan 07 12:10:22 2009 +0100 @@ -203,10 +203,10 @@ (Method.Basic (pat_completeness, Position.none), SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none)))) -fun termination_by method = +fun termination_by method int = FundefPackage.setup_termination_proof NONE #> Proof.future_terminal_proof - (Method.Basic (method, Position.none), NONE) + (Method.Basic (method, Position.none), NONE) int fun mk_catchall fixes arities = let @@ -304,19 +304,19 @@ local structure P = OuterParse and K = OuterKeyword in -fun fun_cmd config fixes statements flags lthy = +fun fun_cmd config fixes statements flags int lthy = let val group = serial_string () in lthy |> LocalTheory.set_group group |> FundefPackage.add_fundef fixes statements config flags - |> by_pat_completeness_simp + |> by_pat_completeness_simp int |> LocalTheory.restore |> LocalTheory.set_group group - |> termination_by (FundefCommon.get_termination_prover (Context.Proof lthy)) + |> termination_by (FundefCommon.get_termination_prover (Context.Proof lthy)) int end; val _ = - OuterSyntax.local_theory "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)) => fun_cmd config fixes statements flags));