src/HOL/thy_syntax.ML
changeset 6555 17b7b88a8e3c
parent 6523 c84935821ba0
child 6576 7e0b35bed503
     1.1 --- a/src/HOL/thy_syntax.ML	Fri Apr 30 18:08:58 1999 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Fri Apr 30 18:09:33 1999 +0200
     1.3 @@ -213,7 +213,7 @@
     1.4  (** TFL with explicit WF relations **)
     1.5  
     1.6  (*fname: name of function being defined; rel: well-founded relation*)
     1.7 -fun mk_rec_decl ((((fname, rel), congs), ss), axms) =
     1.8 +fun mk_recdef_decl ((((fname, rel), congs), ss), axms) =
     1.9    let
    1.10      val fid = strip_quotes fname;
    1.11      val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
    1.12 @@ -233,42 +233,40 @@
    1.13      \val thy = thy\n"
    1.14    end;
    1.15  
    1.16 +val recdef_decl =
    1.17 +  (name -- string --
    1.18 +    optional ("congs" $$-- list1 name) [] --
    1.19 +    optional ("simpset" $$-- string >> strip_quotes) "simpset()" --
    1.20 +    repeat1 string >> mk_recdef_decl);
    1.21 +
    1.22  
    1.23  (** TFL with no WF relation supplied **)
    1.24  
    1.25  (*fname: name of function being defined; rel: well-founded relation*)
    1.26 -fun mk_rec_deferred_decl (((fname, congs), ss), axms) =
    1.27 -  let val fid = strip_quotes fname
    1.28 -      val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
    1.29 +fun mk_defer_recdef_decl ((fname, congs), axms) =
    1.30 +  let
    1.31 +    val fid = strip_quotes fname;
    1.32 +    val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
    1.33 +    val axms_text = mk_big_list axms;
    1.34    in
    1.35 -      ";\n\n\
    1.36 -       \local\n\
    1.37 -       \val (thy, induct_rules) = Tfl.function thy " ^ 
    1.38 -          quote fid ^ " " ^ 
    1.39 -	  " (" ^ congs_text ^ ")\n" 
    1.40 -	  ^ mk_big_list axms ^ ";\n\
    1.41 -       \in\n\
    1.42 -       \structure " ^ fid ^ " =\n\
    1.43 -       \struct\n\
    1.44 -       \  val induct_rules = induct_rules \n\
    1.45 -       \end;\n\
    1.46 -       \val thy = thy;\nend;\n\
    1.47 -       \val thy = thy\n"
    1.48 +    ";\n\n\
    1.49 +    \local\n\
    1.50 +    \val (thy, result) = thy |> RecdefPackage.defer_recdef " ^ quote fid ^ "\n" ^
    1.51 +    axms_text ^ "\n" ^ congs_text ^ ";\n\
    1.52 +    \in\n\
    1.53 +    \structure " ^ fid ^ " =\n\
    1.54 +    \struct\n\
    1.55 +    \  val {induct_rules} = result;\n\
    1.56 +    \end;\n\
    1.57 +    \val thy = thy;\n\
    1.58 +    \end;\n\
    1.59 +    \val thy = thy\n"
    1.60    end;
    1.61  
    1.62 -
    1.63 -(*parses either a standard or a deferred recdef; the latter has no WF
    1.64 -  relation given*)
    1.65 -val recdef_decl = 
    1.66 -    (name -- string -- 
    1.67 -     optional ("congs" $$-- list1 name) [] -- 
    1.68 -     optional ("simpset" $$-- string >> strip_quotes) "simpset()" -- 
    1.69 -     repeat1 string >> mk_rec_decl)
    1.70 -    ||
    1.71 -    (name --$$ "??" --
    1.72 -     optional ("congs" $$-- list1 name) [] -- 
    1.73 -     optional ("simpset" $$-- string >> strip_quotes) "simpset()" -- 
    1.74 -     repeat1 string >> mk_rec_deferred_decl) ;
    1.75 +val defer_recdef_decl =
    1.76 +  (name --
    1.77 +    optional ("congs" $$-- list1 name) [] --
    1.78 +    repeat1 string >> mk_defer_recdef_decl);
    1.79  
    1.80  
    1.81  
    1.82 @@ -278,7 +276,7 @@
    1.83  
    1.84  val _ = ThySyn.add_syntax
    1.85   ["intrs", "monos", "con_defs", "congs", "simpset", "|",
    1.86 -  "and", "distinct", "inject", "induct", "??"]
    1.87 +  "and", "distinct", "inject", "induct"]
    1.88   [axm_section "typedef" "|> TypedefPackage.add_typedef" typedef_decl,
    1.89    section "record" "|> (#1 oooo RecordPackage.add_record)" record_decl,
    1.90    section "inductive" 	"" (inductive_decl false),
    1.91 @@ -286,6 +284,7 @@
    1.92    section "datatype" 	"" datatype_decl,
    1.93    section "rep_datatype" "" rep_datatype_decl,
    1.94    section "primrec" 	"" primrec_decl,
    1.95 -  section "recdef" 	"" recdef_decl];
    1.96 +  section "recdef" 	"" recdef_decl,
    1.97 +  section "defer_recdef" "" defer_recdef_decl];
    1.98  
    1.99  end;