src/HOL/thy_syntax.ML

--- a/src/HOL/thy_syntax.ML	Fri Apr 30 18:08:58 1999 +0200
+++ b/src/HOL/thy_syntax.ML	Fri Apr 30 18:09:33 1999 +0200
@@ -213,7 +213,7 @@
 (** TFL with explicit WF relations **)
 
 (*fname: name of function being defined; rel: well-founded relation*)
-fun mk_rec_decl ((((fname, rel), congs), ss), axms) =
+fun mk_recdef_decl ((((fname, rel), congs), ss), axms) =
   let
     val fid = strip_quotes fname;
     val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
@@ -233,42 +233,40 @@
     \val thy = thy\n"
   end;
 
+val recdef_decl =
+  (name -- string --
+    optional ("congs" $$-- list1 name) [] --
+    optional ("simpset" $$-- string >> strip_quotes) "simpset()" --
+    repeat1 string >> mk_recdef_decl);
+
 
 (** TFL with no WF relation supplied **)
 
 (*fname: name of function being defined; rel: well-founded relation*)
-fun mk_rec_deferred_decl (((fname, congs), ss), axms) =
-  let val fid = strip_quotes fname
-      val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
+fun mk_defer_recdef_decl ((fname, congs), axms) =
+  let
+    val fid = strip_quotes fname;
+    val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
+    val axms_text = mk_big_list axms;
   in
-      ";\n\n\
-       \local\n\
-       \val (thy, induct_rules) = Tfl.function thy " ^ 
-          quote fid ^ " " ^ 
-	  " (" ^ congs_text ^ ")\n" 
-	  ^ mk_big_list axms ^ ";\n\
-       \in\n\
-       \structure " ^ fid ^ " =\n\
-       \struct\n\
-       \  val induct_rules = induct_rules \n\
-       \end;\n\
-       \val thy = thy;\nend;\n\
-       \val thy = thy\n"
+    ";\n\n\
+    \local\n\
+    \val (thy, result) = thy |> RecdefPackage.defer_recdef " ^ quote fid ^ "\n" ^
+    axms_text ^ "\n" ^ congs_text ^ ";\n\
+    \in\n\
+    \structure " ^ fid ^ " =\n\
+    \struct\n\
+    \  val {induct_rules} = result;\n\
+    \end;\n\
+    \val thy = thy;\n\
+    \end;\n\
+    \val thy = thy\n"
   end;
 
-
-(*parses either a standard or a deferred recdef; the latter has no WF
-  relation given*)
-val recdef_decl = 
-    (name -- string -- 
-     optional ("congs" $$-- list1 name) [] -- 
-     optional ("simpset" $$-- string >> strip_quotes) "simpset()" -- 
-     repeat1 string >> mk_rec_decl)
-    ||
-    (name --$$ "??" --
-     optional ("congs" $$-- list1 name) [] -- 
-     optional ("simpset" $$-- string >> strip_quotes) "simpset()" -- 
-     repeat1 string >> mk_rec_deferred_decl) ;
+val defer_recdef_decl =
+  (name --
+    optional ("congs" $$-- list1 name) [] --
+    repeat1 string >> mk_defer_recdef_decl);
 
 
 
@@ -278,7 +276,7 @@
 
 val _ = ThySyn.add_syntax
  ["intrs", "monos", "con_defs", "congs", "simpset", "|",
-  "and", "distinct", "inject", "induct", "??"]
+  "and", "distinct", "inject", "induct"]
  [axm_section "typedef" "|> TypedefPackage.add_typedef" typedef_decl,
   section "record" "|> (#1 oooo RecordPackage.add_record)" record_decl,
   section "inductive" 	"" (inductive_decl false),
@@ -286,6 +284,7 @@
   section "datatype" 	"" datatype_decl,
   section "rep_datatype" "" rep_datatype_decl,
   section "primrec" 	"" primrec_decl,
-  section "recdef" 	"" recdef_decl];
+  section "recdef" 	"" recdef_decl,
+  section "defer_recdef" "" defer_recdef_decl];
 
 end;