src/HOL/Tools/function_package/fundef_package.ML
changeset 20338 ecdfc96cf4d0
parent 20320 a5368278a72c
child 20363 f34c5dbe74d5
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Aug 04 12:01:31 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Aug 04 18:01:45 2006 +0200
     1.3 @@ -85,11 +85,6 @@
     1.4        val spec = map prep_eqns eqns_attss
     1.5        val t_eqnss = map (flat o map snd) spec
     1.6  
     1.7 -(*
     1.8 - val t_eqns = if preprocess then map (FundefSplit.split_all_equations (ProofContext.init thy)) t_eqns
     1.9 -              else t_eqns
    1.10 -*)
    1.11 -
    1.12        val congs = get_fundef_congs (Context.Theory thy)
    1.13  
    1.14        val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqnss thy
    1.15 @@ -218,16 +213,16 @@
    1.16  
    1.17  val opt_attribs_with_star = Scan.optional attribs_with_star ([], false);
    1.18  
    1.19 -fun opt_thm_name_star s =
    1.20 -  Scan.optional ((P.name -- opt_attribs_with_star || (attribs_with_star >> pair "")) --| P.$$$ s) ("", ([], false));
    1.21 +val opt_thm_name_star =
    1.22 +  Scan.optional ((P.name -- opt_attribs_with_star || (attribs_with_star >> pair "")) --| P.$$$ ":") ("", ([], false));
    1.23  
    1.24  
    1.25  val function_decl =
    1.26 -    Scan.repeat1 (opt_thm_name_star ":" -- P.prop);
    1.27 +    Scan.repeat1 (opt_thm_name_star -- P.prop);
    1.28  
    1.29  val functionP =
    1.30    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
    1.31 -  (((Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "pre" -- P.$$$ ")") >> K true) false) --    
    1.32 +  (((Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "sequential" -- P.$$$ ")") >> K true) false) --    
    1.33    P.and_list1 function_decl) >> (fn (prepr, eqnss) =>
    1.34                                      Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss prepr)));
    1.35  
    1.36 @@ -237,6 +232,8 @@
    1.37         >> (fn (name,dom) =>
    1.38  	      Toplevel.print o Toplevel.theory_to_proof (fundef_setup_termination_proof name dom)));
    1.39  
    1.40 +val _ = OuterSyntax.add_keywords ["sequential", "otherwise"];
    1.41 +
    1.42  val _ = OuterSyntax.add_parsers [functionP];
    1.43  val _ = OuterSyntax.add_parsers [terminationP];
    1.44