# HG changeset patch
# User paulson
# Date 924862950 -7200
# Node ID 120ca2bb27e1021ce7961af307b33491b3ad9851
# Parent  a185927883e525cd17ec2bbd6b15909f118205eb
Now for recdefs that omit the WF relation

diff -r a185927883e5 -r 120ca2bb27e1 src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Fri Apr 23 12:20:22 1999 +0200
+++ b/src/HOL/thy_syntax.ML	Fri Apr 23 12:22:30 1999 +0200
@@ -208,11 +208,12 @@
   (repeat1 ((ident -- string) || (string >> pair "")))) >> mk_primrec_decl;
 
 
+(*** recdef: interface to Slind's TFL ***)
 
-(** recdef: interface to Slind's TFL **)
+(** TFL with explicit WF relations **)
 
 (*fname: name of function being defined; rel: well-founded relation*)
-fun mk_recdef_decl ((((fname, rel), congs), ss), axms) =
+fun mk_rec_decl ((((fname, rel), congs), ss), axms) =
   let
     val fid = strip_quotes fname;
     val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
@@ -232,11 +233,42 @@
     \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);
+  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"
+  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) ;
 
 
 
@@ -246,14 +278,14 @@
 
 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" "|> RecordPackage.add_record" record_decl,
-  section "inductive" "" (inductive_decl false),
-  section "coinductive" "" (inductive_decl true),
-  section "datatype" "" datatype_decl,
+  section "inductive" 	"" (inductive_decl false),
+  section "coinductive"	"" (inductive_decl true),
+  section "datatype" 	"" datatype_decl,
   section "rep_datatype" "" rep_datatype_decl,
-  section "primrec" "" primrec_decl,
-  section "recdef" "" recdef_decl];
+  section "primrec" 	"" primrec_decl,
+  section "recdef" 	"" recdef_decl];
 
 end;