src/HOL/Tools/recdef_package.ML
changeset 6478 48f90bc10cf5
parent 6458 13c779aec65a
child 6520 08637598f7ec
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Thu Apr 22 12:49:34 1999 +0200
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Thu Apr 22 12:50:39 1999 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4    val print_recdefs: theory -> unit
     1.5    val get_recdef: theory -> string -> {rules: thm list, induct: thm, tcs: term list}
     1.6    val add_recdef: xstring -> string -> ((bstring * string) * Args.src list) list
     1.7 -    -> string option -> (xstring * Args.src list) list
     1.8 +    -> simpset option -> (xstring * Args.src list) list
     1.9      -> theory -> theory * {rules: thm list, induct: thm, tcs: term list}
    1.10    val add_recdef_i: xstring -> term -> ((bstring * term) * theory attribute list) list
    1.11      -> simpset option -> (thm * theory attribute list) list
    1.12 @@ -77,6 +77,7 @@
    1.13      val name = Sign.intern_const (Theory.sign_of thy) raw_name;
    1.14      val bname = Sign.base_name name;
    1.15  
    1.16 +    val _ = Theory.requires thy "Recdef" "recursive function definitions";
    1.17      val _ = message ("Defining recursive function " ^ quote name ^ " ...");
    1.18  
    1.19      val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
    1.20 @@ -94,9 +95,9 @@
    1.21        |> Theory.parent_path;
    1.22    in (thy3, result) end;
    1.23  
    1.24 -val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute
    1.25 +val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute I IsarThy.apply_theorems;
    1.26 +val add_recdef_x = gen_add_recdef Tfl.define Attrib.global_attribute
    1.27    (Simplifier.simpset_of o ThyInfo.get_theory) IsarThy.apply_theorems;
    1.28 -
    1.29  val add_recdef_i = gen_add_recdef Tfl.define_i (K I) I IsarThy.apply_theorems_i;
    1.30  
    1.31  
    1.32 @@ -113,9 +114,9 @@
    1.33  
    1.34  val recdef_decl =
    1.35    name -- term -- Scan.repeat1 (opt_thm_name ":" -- term) --
    1.36 -  Scan.optional ($$$ "congs" |-- !!! xthms1) [] --
    1.37 -  Scan.option ($$$ "simpset" |-- !!! name)
    1.38 -  >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef f R (map triple_swap eqs) ss congs);
    1.39 +  Scan.optional ($$$ "(" |-- $$$ "congs" |-- !!! (xthms1 --| $$$ ")")) [] --
    1.40 +  Scan.option ($$$ "(" |-- $$$ "simpset" |-- !!! (name --| $$$ ")"))
    1.41 +  >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef_x f R (map triple_swap eqs) ss congs);
    1.42  
    1.43  val recdefP =
    1.44    OuterSyntax.command "recdef" "define general recursive functions (TFL)"