src/HOL/Tools/function_package/fundef_package.ML
changeset 20654 d80502f0d701
parent 20638 241792a4634e
child 20877 368b997ad67e
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Sep 21 03:17:51 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Sep 21 12:22:05 2006 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  sig
     1.5      val add_fundef :  (string * string option * mixfix) list 
     1.6                        -> ((bstring * Attrib.src list) * string list) list list
     1.7 -                      -> bool 
     1.8 +                      -> FundefCommon.fundef_config 
     1.9                        -> local_theory 
    1.10                        -> Proof.state
    1.11  
    1.12 @@ -34,6 +34,7 @@
    1.13  
    1.14  open FundefCommon
    1.15  
    1.16 +(*fn (ctxt,s) => Variable.importT_terms (fst (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) [] [s])) ctxt;*)
    1.17  
    1.18  fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *)
    1.19      let val (xs, ys) = split_list ps
    1.20 @@ -101,14 +102,16 @@
    1.21      end
    1.22  
    1.23  
    1.24 -fun gen_add_fundef prep_spec fixspec eqnss_flags preprocess lthy =
    1.25 +fun gen_add_fundef prep_spec fixspec eqnss_flags config lthy =
    1.26      let
    1.27 -      val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags preprocess lthy
    1.28 +      val FundefConfig {sequential, default, ...} = config
    1.29 +
    1.30 +      val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags sequential lthy
    1.31        val t_eqns = spec
    1.32                       |> flat |> map snd |> flat (* flatten external structure *)
    1.33  
    1.34        val ((mutual_info, name, prep_result as Prep {goal, goalI, ...}), lthy) = 
    1.35 -          FundefMutual.prepare_fundef_mutual fixes t_eqns lthy
    1.36 +          FundefMutual.prepare_fundef_mutual fixes t_eqns default lthy
    1.37  
    1.38        val afterqed = fundef_afterqed fixes spec mutual_info name prep_result
    1.39      in
    1.40 @@ -198,9 +201,9 @@
    1.41  
    1.42  val functionP =
    1.43    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
    1.44 -  ((opt_sequential -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
    1.45 -     >> (fn (((sequential, target), fixes), statements) =>
    1.46 -            Toplevel.print o local_theory_to_proof (add_fundef fixes statements sequential)));
    1.47 +  ((config_parser -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
    1.48 +     >> (fn (((config, target), fixes), statements) =>
    1.49 +            Toplevel.print o local_theory_to_proof (add_fundef fixes statements config)));
    1.50  
    1.51  
    1.52  val terminationP =
    1.53 @@ -211,7 +214,7 @@
    1.54  
    1.55  val _ = OuterSyntax.add_parsers [functionP];
    1.56  val _ = OuterSyntax.add_parsers [terminationP];
    1.57 -val _ = OuterSyntax.add_keywords ["sequential", "otherwise"]; (* currently unused *)
    1.58 +val _ = OuterSyntax.add_keywords ["sequential", "otherwise"];
    1.59  
    1.60  end;
    1.61