src/HOL/thy_syntax.ML
changeset 9857 2f994c499bef
parent 8813 abc0f3722aed
child 11628 e57a6e51715e
     1.1 --- a/src/HOL/thy_syntax.ML	Tue Sep 05 18:48:22 2000 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Tue Sep 05 18:48:41 2000 +0200
     1.3 @@ -220,15 +220,12 @@
     1.4  
     1.5  (*fname: name of function being defined; rel: well-founded relation*)
     1.6  fun mk_recdef_decl ((((fname, rel), congs), ss), eqns) =
     1.7 -  let
     1.8 -    val fid = unenclose fname;
     1.9 -    val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
    1.10 -  in
    1.11 +  let val fid = unenclose fname in
    1.12      ";\n\n\
    1.13      \local\n\
    1.14      \fun simpset() = Simplifier.simpset_of thy;\n\
    1.15 -    \val (thy, result) = thy |> RecdefPackage.add_recdef " ^ quote fid ^ " " ^ rel ^ "\n" ^
    1.16 -    mk_eqns eqns ^ "\n(Some (" ^ ss ^ "))\n" ^ congs_text ^ ";\n\
    1.17 +    \val (thy, result) = thy |> RecdefPackage.add_recdef_old " ^ quote fid ^ " " ^ rel ^ "\n" ^
    1.18 +    mk_eqns eqns ^ "\n(" ^ ss ^ ",\n " ^ mk_list congs ^ ");\n\
    1.19      \in\n\
    1.20      \structure " ^ fid ^ " =\n\
    1.21      \struct\n\
    1.22 @@ -241,7 +238,7 @@
    1.23  
    1.24  val recdef_decl =
    1.25    name -- string --
    1.26 -    optional ("congs" $$-- list1 name) [] --
    1.27 +    optional ("congs" $$-- list1 ident) [] --
    1.28      optional ("simpset" $$-- string >> unenclose) "simpset()" --
    1.29      repeat1 (ident -- string || (string >> pair "")) >> mk_recdef_decl;
    1.30