src/HOL/thy_syntax.ML
changeset 8657 b9475dad85ed
parent 8623 5668aaf41c36
child 8813 abc0f3722aed
     1.1 --- a/src/HOL/thy_syntax.ML	Sat Apr 01 20:18:52 2000 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Sat Apr 01 20:21:39 2000 +0200
     1.3 @@ -193,19 +193,17 @@
     1.4  
     1.5  (** primrec **)
     1.6  
     1.7 +fun mk_patterns eqns = mk_list (map (fn (s, _) => if s = "" then "_" else s) eqns);
     1.8 +fun mk_eqns eqns = mk_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) eqns);
     1.9 +
    1.10  fun mk_primrec_decl (alt_name, eqns) =
    1.11 -  let
    1.12 -    val names = map (fn (s, _) => if s = "" then "_" else s) eqns
    1.13 -  in
    1.14 -    ";\nval (thy, " ^ mk_list names ^ ") = PrimrecPackage.add_primrec " ^ alt_name ^ " " ^
    1.15 -    mk_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) eqns) ^
    1.16 -    " " ^ " thy;\n\
    1.17 -    \val thy = thy\n"
    1.18 -  end;
    1.19 +  ";\nval (thy, " ^ mk_patterns eqns ^ ") = PrimrecPackage.add_primrec " ^ alt_name ^ " "
    1.20 +  ^ mk_eqns eqns ^ " " ^ " thy;\n\
    1.21 +  \val thy = thy\n"
    1.22  
    1.23  (* either names and axioms or just axioms *)
    1.24 -val primrec_decl = (optional ("(" $$-- name --$$ ")") "\"\"" --
    1.25 -  (repeat1 ((ident -- string) || (string >> pair "")))) >> mk_primrec_decl;
    1.26 +val primrec_decl = optional ("(" $$-- name --$$ ")") "\"\"" --
    1.27 +  repeat1 (ident -- string || (string >> pair "")) >> mk_primrec_decl;
    1.28  
    1.29  
    1.30  (*** recdef: interface to Slind's TFL ***)
    1.31 @@ -213,21 +211,20 @@
    1.32  (** TFL with explicit WF relations **)
    1.33  
    1.34  (*fname: name of function being defined; rel: well-founded relation*)
    1.35 -fun mk_recdef_decl ((((fname, rel), congs), ss), axms) =
    1.36 +fun mk_recdef_decl ((((fname, rel), congs), ss), eqns) =
    1.37    let
    1.38      val fid = unenclose fname;
    1.39      val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
    1.40 -    val axms_text = mk_big_list axms;
    1.41    in
    1.42      ";\n\n\
    1.43      \local\n\
    1.44      \fun simpset() = Simplifier.simpset_of thy;\n\
    1.45      \val (thy, result) = thy |> RecdefPackage.add_recdef " ^ quote fid ^ " " ^ rel ^ "\n" ^
    1.46 -    axms_text ^ "\n(Some (" ^ ss ^ "))\n" ^ congs_text ^ ";\n\
    1.47 +    mk_eqns eqns ^ "\n(Some (" ^ ss ^ "))\n" ^ congs_text ^ ";\n\
    1.48      \in\n\
    1.49      \structure " ^ fid ^ " =\n\
    1.50      \struct\n\
    1.51 -    \  val {simps, induct, tcs} = result;\n\
    1.52 +    \  val {simps, rules = " ^ mk_patterns eqns ^ ", induct, tcs} = result;\n\
    1.53      \end;\n\
    1.54      \val thy = thy;\n\
    1.55      \end;\n\
    1.56 @@ -235,10 +232,10 @@
    1.57    end;
    1.58  
    1.59  val recdef_decl =
    1.60 -  (name -- string --
    1.61 +  name -- string --
    1.62      optional ("congs" $$-- list1 name) [] --
    1.63      optional ("simpset" $$-- string >> unenclose) "simpset()" --
    1.64 -    repeat1 string >> mk_recdef_decl);
    1.65 +    repeat1 (ident -- string || (string >> pair "")) >> mk_recdef_decl;
    1.66  
    1.67  
    1.68  (** TFL with no WF relation supplied **)