get_tthms witness theorems;
authorwenzelm
Tue Jan 12 16:42:21 1999 +0100 (1999-01-12)
changeset 610336f272ea9413
parent 6102 b985e2184868
child 6104 55c7f8f0bb4d
get_tthms witness theorems;
src/HOL/Tools/datatype_package.ML
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Jan 12 16:00:31 1999 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Jan 12 16:42:21 1999 +0100
     1.3 @@ -31,18 +31,7 @@
     1.4         induction : thm,
     1.5         size : thm list,
     1.6         simps : thm list}
     1.7 -  val rep_datatype : string list option -> xstring list list ->
     1.8 -    xstring list list -> xstring -> theory -> theory *
     1.9 -      {distinct : thm list list,
    1.10 -       inject : thm list list,
    1.11 -       exhaustion : thm list,
    1.12 -       rec_thms : thm list,
    1.13 -       case_thms : thm list list,
    1.14 -       split_thms : (thm * thm) list,
    1.15 -       induction : thm,
    1.16 -       size : thm list,
    1.17 -       simps : thm list}
    1.18 -  val rep_datatype_i : string list option -> thm list list ->
    1.19 +  val rep_datatype : string list option -> thm list list ->
    1.20      thm list list -> thm -> theory -> theory *
    1.21        {distinct : thm list list,
    1.22         inject : thm list list,
    1.23 @@ -483,14 +472,10 @@
    1.24  
    1.25  (*********************** declare non-datatype as datatype *********************)
    1.26  
    1.27 -fun gen_rep_datatype get get' alt_names distinct_names inject_names induction_name thy =
    1.28 +fun rep_datatype alt_names distinct inject induction thy =
    1.29    let
    1.30      val sign = sign_of thy;
    1.31  
    1.32 -    val distinct = map (get thy) distinct_names;
    1.33 -    val inject = map (get thy) inject_names;
    1.34 -    val induction = get' thy induction_name;
    1.35 -
    1.36      val induction' = freezeT induction;
    1.37  
    1.38      fun err t = error ("Ill-formed predicate in induction rule: " ^
    1.39 @@ -571,8 +556,6 @@
    1.40        simps = simps})
    1.41    end;
    1.42  
    1.43 -val rep_datatype = gen_rep_datatype (fn thy => PureThy.get_thmss thy) get_thm;
    1.44 -val rep_datatype_i = gen_rep_datatype (K I) (K I);
    1.45  
    1.46  (******************************** add datatype ********************************)
    1.47  
     2.1 --- a/src/HOL/thy_syntax.ML	Tue Jan 12 16:00:31 1999 +0100
     2.2 +++ b/src/HOL/thy_syntax.ML	Tue Jan 12 16:42:21 1999 +0100
     2.3 @@ -134,22 +134,25 @@
     2.4        ";\nlocal\n\
     2.5        \val (thy, {distinct, inject, exhaustion, rec_thms,\n\
     2.6        \  case_thms, split_thms, induction, size, simps}) =\n\
     2.7 -      \  DatatypePackage.add_datatype false " ^ add_datatype_args ^ " thy;\n\
     2.8 +      \ DatatypePackage.add_datatype false " ^ add_datatype_args ^ " thy;\n\
     2.9        \in\n" ^ mk_bind_thms_string names ^
    2.10        "val thy = thy;\nend;\nval thy = thy\n"
    2.11      end;
    2.12  
    2.13 +  fun mk_thmss namess = "(map (PureThy.get_thmss thy) " ^ mk_list (map mk_list namess) ^ ")";
    2.14 +  fun mk_thm name = "(PureThy.get_thm thy " ^ name ^ ")";
    2.15 +
    2.16    fun mk_rep_dt_string (((names, distinct), inject), induct) =
    2.17      ";\nlocal\n\
    2.18      \val (thy, {distinct, inject, exhaustion, rec_thms,\n\
    2.19      \  case_thms, split_thms, induction, size, simps}) =\n\
    2.20 -    \  DatatypePackage.rep_datatype " ^
    2.21 +    \ DatatypePackage.rep_datatype " ^
    2.22      (case names of
    2.23 -        Some names => "(Some [" ^ commas_quote names ^ "]) " ^
    2.24 -          mk_list (map mk_list distinct) ^ " " ^ mk_list (map mk_list inject) ^
    2.25 -            " " ^ induct ^ " thy;\nin\n" ^ mk_bind_thms_string names
    2.26 -      | None => "None " ^ mk_list (map mk_list distinct) ^ " " ^
    2.27 -          mk_list (map mk_list inject) ^ " " ^ induct ^ " thy;\nin\n") ^
    2.28 +        Some names => "(Some [" ^ commas_quote names ^ "])\n " ^
    2.29 +          mk_thmss distinct ^ "\n " ^ mk_thmss inject ^
    2.30 +            "\n " ^ mk_thm induct ^ " thy;\nin\n" ^ mk_bind_thms_string names
    2.31 +      | None => "None\n " ^ mk_thmss distinct ^ "\n " ^ mk_thmss inject ^
    2.32 +            "\n " ^ mk_thm induct ^ " thy;\nin\n") ^
    2.33      "val thy = thy;\nend;\nval thy = thy\n";
    2.34  
    2.35    (*** parsers ***)