# HG changeset patch
# User wenzelm
# Date 925827496 -7200
# Node ID 7e0b35bed5030f85134113726f56b9d8523e5241
# Parent  70d758762c501644d9a9d0f54ff698761c057d1e
add_recdef: removed names / attributes;

diff -r 70d758762c50 -r 7e0b35bed503 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Tue May 04 13:47:28 1999 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Tue May 04 16:18:16 1999 +0200
@@ -10,11 +10,11 @@
   val quiet_mode: bool ref
   val print_recdefs: theory -> unit
   val get_recdef: theory -> string -> {rules: thm list, induct: thm, tcs: term list}
-  val add_recdef: xstring -> string -> ((bstring * string) * Args.src list) list
-    -> simpset option -> (xstring * Args.src list) list
-    -> theory -> theory * {rules: thm list, induct: thm, tcs: term list}
-  val add_recdef_i: xstring -> term -> ((bstring * term) * theory attribute list) list
-    -> simpset option -> (thm * theory attribute list) list
+  val add_recdef: xstring -> string -> string list -> simpset option
+    -> (xstring * Args.src list) list -> theory
+    -> theory * {rules: thm list, induct: thm, tcs: term list}
+  val add_recdef_i: xstring -> term -> term list -> simpset option
+    -> (thm * theory attribute list) list
     -> theory -> theory * {rules: thm list, induct: thm, tcs: term list}
   val defer_recdef: xstring -> string list -> (xstring * Args.src list) list
     -> theory -> theory * {induct_rules: thm}
@@ -75,7 +75,7 @@
 
 fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions";
 
-fun gen_add_recdef tfl_fn prep_att prep_ss app_thms raw_name R eq_srcs raw_ss raw_congs thy =
+fun gen_add_recdef tfl_fn prep_ss app_thms raw_name R eqs raw_ss raw_congs thy =
   let
     val name = Sign.intern_const (Theory.sign_of thy) raw_name;
     val bname = Sign.base_name name;
@@ -83,8 +83,6 @@
     val _ = requires_recdef thy;
     val _ = message ("Defining recursive function " ^ quote name ^ " ...");
 
-    val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
-    val eq_atts = map (map (prep_att thy)) raw_eq_atts;
     val ss = (case raw_ss of None => Simplifier.simpset_of thy | Some x => prep_ss x);
     val (thy1, congs) = thy |> app_thms raw_congs;
     val (thy2, pats) = tfl_fn thy1 name R eqs;
@@ -93,15 +91,15 @@
       thy2
       |> Theory.add_path bname
       |> PureThy.add_thmss [(("rules", rules), [])]
-      |> PureThy.add_thms ((("induct", induct), []) :: ((eq_names ~~ rules) ~~ eq_atts))
+      |> PureThy.add_thms [(("induct", induct), [])]
       |> put_recdef name result
       |> Theory.parent_path;
   in (thy3, result) end;
 
-val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute I IsarThy.apply_theorems;
-val add_recdef_x = gen_add_recdef Tfl.define Attrib.global_attribute
-  (Simplifier.simpset_of o ThyInfo.get_theory) IsarThy.apply_theorems;
-val add_recdef_i = gen_add_recdef Tfl.define_i (K I) I IsarThy.apply_theorems_i;
+val add_recdef = gen_add_recdef Tfl.define I IsarThy.apply_theorems;
+val add_recdef_x = gen_add_recdef Tfl.define (Simplifier.simpset_of o ThyInfo.get_theory)
+  IsarThy.apply_theorems;
+val add_recdef_i = gen_add_recdef Tfl.define_i I IsarThy.apply_theorems_i;
 
 
 
@@ -141,10 +139,10 @@
 local open OuterParse in
 
 val recdef_decl =
-  name -- term -- Scan.repeat1 (opt_thm_name ":" -- term) --
+  name -- term -- Scan.repeat1 term --
   Scan.optional ($$$ "(" |-- $$$ "congs" |-- !!! (xthms1 --| $$$ ")")) [] --
   Scan.option ($$$ "(" |-- $$$ "simpset" |-- !!! (name --| $$$ ")"))
-  >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef_x f R (map triple_swap eqs) ss congs);
+  >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef_x f R eqs ss congs);
 
 val recdefP =
   OuterSyntax.command "recdef" "define general recursive functions (TFL)"
diff -r 70d758762c50 -r 7e0b35bed503 src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Tue May 04 13:47:28 1999 +0200
+++ b/src/HOL/thy_syntax.ML	Tue May 04 16:18:16 1999 +0200
@@ -217,7 +217,7 @@
   let
     val fid = strip_quotes fname;
     val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
-    val axms_text = mk_big_list (map (fn a => mk_pair (mk_pair (quote "", a), "[]")) axms);
+    val axms_text = mk_big_list axms;
   in
     ";\n\n\
     \local\n\