add_recdef: removed names / attributes;
authorwenzelm
Tue May 04 16:18:16 1999 +0200 (1999-05-04)
changeset 65767e0b35bed503
parent 6575 70d758762c50
child 6577 a2b5c84d590a
add_recdef: removed names / attributes;
src/HOL/Tools/recdef_package.ML
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Tue May 04 13:47:28 1999 +0200
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Tue May 04 16:18:16 1999 +0200
     1.3 @@ -10,11 +10,11 @@
     1.4    val quiet_mode: bool ref
     1.5    val print_recdefs: theory -> unit
     1.6    val get_recdef: theory -> string -> {rules: thm list, induct: thm, tcs: term list}
     1.7 -  val add_recdef: xstring -> string -> ((bstring * string) * 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 +  val add_recdef: xstring -> string -> string list -> simpset option
    1.13 +    -> (xstring * Args.src list) list -> theory
    1.14 +    -> theory * {rules: thm list, induct: thm, tcs: term list}
    1.15 +  val add_recdef_i: xstring -> term -> term list -> simpset option
    1.16 +    -> (thm * theory attribute list) list
    1.17      -> theory -> theory * {rules: thm list, induct: thm, tcs: term list}
    1.18    val defer_recdef: xstring -> string list -> (xstring * Args.src list) list
    1.19      -> theory -> theory * {induct_rules: thm}
    1.20 @@ -75,7 +75,7 @@
    1.21  
    1.22  fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions";
    1.23  
    1.24 -fun gen_add_recdef tfl_fn prep_att prep_ss app_thms raw_name R eq_srcs raw_ss raw_congs thy =
    1.25 +fun gen_add_recdef tfl_fn prep_ss app_thms raw_name R eqs raw_ss raw_congs thy =
    1.26    let
    1.27      val name = Sign.intern_const (Theory.sign_of thy) raw_name;
    1.28      val bname = Sign.base_name name;
    1.29 @@ -83,8 +83,6 @@
    1.30      val _ = requires_recdef thy;
    1.31      val _ = message ("Defining recursive function " ^ quote name ^ " ...");
    1.32  
    1.33 -    val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
    1.34 -    val eq_atts = map (map (prep_att thy)) raw_eq_atts;
    1.35      val ss = (case raw_ss of None => Simplifier.simpset_of thy | Some x => prep_ss x);
    1.36      val (thy1, congs) = thy |> app_thms raw_congs;
    1.37      val (thy2, pats) = tfl_fn thy1 name R eqs;
    1.38 @@ -93,15 +91,15 @@
    1.39        thy2
    1.40        |> Theory.add_path bname
    1.41        |> PureThy.add_thmss [(("rules", rules), [])]
    1.42 -      |> PureThy.add_thms ((("induct", induct), []) :: ((eq_names ~~ rules) ~~ eq_atts))
    1.43 +      |> PureThy.add_thms [(("induct", induct), [])]
    1.44        |> put_recdef name result
    1.45        |> Theory.parent_path;
    1.46    in (thy3, result) end;
    1.47  
    1.48 -val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute I IsarThy.apply_theorems;
    1.49 -val add_recdef_x = gen_add_recdef Tfl.define Attrib.global_attribute
    1.50 -  (Simplifier.simpset_of o ThyInfo.get_theory) IsarThy.apply_theorems;
    1.51 -val add_recdef_i = gen_add_recdef Tfl.define_i (K I) I IsarThy.apply_theorems_i;
    1.52 +val add_recdef = gen_add_recdef Tfl.define I IsarThy.apply_theorems;
    1.53 +val add_recdef_x = gen_add_recdef Tfl.define (Simplifier.simpset_of o ThyInfo.get_theory)
    1.54 +  IsarThy.apply_theorems;
    1.55 +val add_recdef_i = gen_add_recdef Tfl.define_i I IsarThy.apply_theorems_i;
    1.56  
    1.57  
    1.58  
    1.59 @@ -141,10 +139,10 @@
    1.60  local open OuterParse in
    1.61  
    1.62  val recdef_decl =
    1.63 -  name -- term -- Scan.repeat1 (opt_thm_name ":" -- term) --
    1.64 +  name -- term -- Scan.repeat1 term --
    1.65    Scan.optional ($$$ "(" |-- $$$ "congs" |-- !!! (xthms1 --| $$$ ")")) [] --
    1.66    Scan.option ($$$ "(" |-- $$$ "simpset" |-- !!! (name --| $$$ ")"))
    1.67 -  >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef_x f R (map triple_swap eqs) ss congs);
    1.68 +  >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef_x f R eqs ss congs);
    1.69  
    1.70  val recdefP =
    1.71    OuterSyntax.command "recdef" "define general recursive functions (TFL)"
     2.1 --- a/src/HOL/thy_syntax.ML	Tue May 04 13:47:28 1999 +0200
     2.2 +++ b/src/HOL/thy_syntax.ML	Tue May 04 16:18:16 1999 +0200
     2.3 @@ -217,7 +217,7 @@
     2.4    let
     2.5      val fid = strip_quotes fname;
     2.6      val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
     2.7 -    val axms_text = mk_big_list (map (fn a => mk_pair (mk_pair (quote "", a), "[]")) axms);
     2.8 +    val axms_text = mk_big_list axms;
     2.9    in
    2.10      ";\n\n\
    2.11      \local\n\