src/HOL/thy_syntax.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15906 9cb0a8ffa40d
     1.1 --- a/src/HOL/thy_syntax.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/HOL/thy_syntax.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5  fun mk_typedef_decl (((((opt_name, vs), t), mx), rhs), wt) =
     1.6    let
     1.7 -    val name' = if_none opt_name t;
     1.8 +    val name' = getOpt (opt_name,t);
     1.9      val name = unenclose name';
    1.10    in
    1.11      (cat_lines [name', mk_triple (t, mk_list vs, mx), rhs, wt],
    1.12 @@ -101,11 +101,11 @@
    1.13            fun mk_dt_struct (s, (id, i)) =
    1.14              s ^ "structure " ^ id ^ " =\n\
    1.15              \struct\n\
    1.16 -            \  val distinct = nth_elem (" ^ i ^ ", distinct);\n\
    1.17 -            \  val inject = nth_elem (" ^ i ^ ", inject);\n\
    1.18 -            \  val exhaust = nth_elem (" ^ i ^ ", exhaustion);\n\
    1.19 -            \  val cases = nth_elem (" ^ i ^ ", case_thms);\n\
    1.20 -            \  val (split, split_asm) = nth_elem (" ^ i ^ ", split_thms);\n" ^
    1.21 +            \  val distinct = List.nth (distinct, " ^ i ^ ");\n\
    1.22 +            \  val inject = List.nth (inject, " ^ i ^ ");\n\
    1.23 +            \  val exhaust = List.nth (exhaustion, " ^ i ^ ");\n\
    1.24 +            \  val cases = List.nth (case_thms, " ^ i ^ ");\n\
    1.25 +            \  val (split, split_asm) = List.nth (split_thms, " ^ i ^ ");\n" ^
    1.26                (if length names = 1 then
    1.27                   "  val induct = induction;\n\
    1.28                   \  val recs = rec_thms;\n\
    1.29 @@ -114,7 +114,7 @@
    1.30                 else "") ^
    1.31              "end;\n";
    1.32  
    1.33 -          val structs = foldl mk_dt_struct
    1.34 +          val structs = Library.foldl mk_dt_struct
    1.35              ("", (names ~~ (map string_of_int (0 upto length names - 1))));
    1.36  
    1.37          in
    1.38 @@ -131,7 +131,7 @@
    1.39    fun mk_dt_string dts =
    1.40      let
    1.41        val names = map (fn ((((alt_name, _), name), _), _) =>
    1.42 -        unenclose (if_none alt_name name)) dts;
    1.43 +        unenclose (getOpt (alt_name,name))) dts;
    1.44  
    1.45        val add_datatype_args = brackets (commas (map Library.quote names)) ^ " " ^
    1.46          brackets (commas (map (fn ((((_, vs), name), mx), cs) =>