added Konrad's code for the datatype package
authorclasohm
Fri Apr 19 11:33:24 1996 +0200 (1996-04-19)
changeset 16688ead1fe65aad
parent 1667 6056e9c967d9
child 1669 e56cdf711729
added Konrad's code for the datatype package
src/HOL/HOL.ML
src/HOL/datatype.ML
src/HOL/thy_data.ML
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/HOL.ML	Fri Apr 19 11:18:59 1996 +0200
     1.2 +++ b/src/HOL/HOL.ML	Fri Apr 19 11:33:24 1996 +0200
     1.3 @@ -408,12 +408,17 @@
     1.4       ("simpset", ThyMethods {merge = merge, put = put, get = get})
     1.5  end;
     1.6  
     1.7 -exception DT_DATA of string list;
     1.8 -val datatypes = ref [] : string list ref;
     1.9 +
    1.10 +type dtype_info = {case_const:term, case_rewrites:thm list,
    1.11 +                   constructors:term list, nchotomy:thm, case_cong:thm};
    1.12 +
    1.13 +exception DT_DATA of (string * dtype_info) list;
    1.14 +val datatypes = ref [] : (string * dtype_info) list ref;
    1.15  
    1.16  let fun merge [] = DT_DATA []
    1.17 -      | merge ds = let val ds = map (fn DT_DATA x => x) ds;
    1.18 -                   in DT_DATA (foldl (op union) (hd ds, tl ds)) end;
    1.19 +      | merge ds =
    1.20 +          let val ds = map (fn DT_DATA x => x) ds;
    1.21 +          in DT_DATA (foldl (gen_union eq_fst) (hd ds, tl ds)) end;
    1.22  
    1.23      fun put (DT_DATA ds) = datatypes := ds;
    1.24  
     2.1 --- a/src/HOL/datatype.ML	Fri Apr 19 11:18:59 1996 +0200
     2.2 +++ b/src/HOL/datatype.ML	Fri Apr 19 11:33:24 1996 +0200
     2.3 @@ -1,6 +1,7 @@
     2.4  (* Title:       HOL/datatype.ML
     2.5     ID:          $Id$
     2.6 -   Author:      Max Breitling, Carsten Clasohm, Tobias Nipkow, Norbert Voelker
     2.7 +   Author:      Max Breitling, Carsten Clasohm, Tobias Nipkow, Norbert Voelker,
     2.8 +                Konrad Slind
     2.9     Copyright 1995 TU Muenchen
    2.10  *)
    2.11  
    2.12 @@ -400,7 +401,6 @@
    2.13          in add_defs_i [defpairT] thy end;
    2.14  
    2.15      in
    2.16 -      datatypes := map (fn (x,_,_) => x) cons_list' @ (!datatypes);
    2.17        (thy |> add_types types
    2.18             |> add_arities arities
    2.19             |> add_consts consts
    2.20 @@ -482,3 +482,369 @@
    2.21    Note the de-Bruijn indices counting the number of lambdas between the
    2.22    variable and its binding. 
    2.23  *)
    2.24 +
    2.25 +
    2.26 +
    2.27 +(* ----------------------------------------------- *)
    2.28 +(* The following has been written by Konrad Slind. *)
    2.29 +
    2.30 +
    2.31 +type dtype_info = {case_const:term, case_rewrites:thm list,
    2.32 +                   constructors:term list, nchotomy:thm, case_cong:thm};
    2.33 +
    2.34 +signature Dtype_sig =
    2.35 +sig
    2.36 +  val build_case_cong: Sign.sg -> thm list -> cterm
    2.37 +  val build_nchotomy: Sign.sg -> thm list -> cterm
    2.38 +
    2.39 +  val prove_case_cong: thm -> thm list -> cterm -> thm
    2.40 +  val prove_nchotomy: (string -> int -> tactic) -> thm list -> cterm -> thm
    2.41 +
    2.42 +  val case_thms : Sign.sg -> thm list -> (string -> int -> tactic)
    2.43 +                   -> {nchotomy:thm, case_cong:thm}
    2.44 +
    2.45 +  val build_record : (theory * (string * string list)
    2.46 +                      * (string -> int -> tactic))
    2.47 +                     -> (string * dtype_info) 
    2.48 +
    2.49 +end;
    2.50 +
    2.51 +
    2.52 +(*---------------------------------------------------------------------------
    2.53 + * This structure is support for the Isabelle datatype package. It provides
    2.54 + * entrypoints for 1) building and proving the case congruence theorem for
    2.55 + * a datatype and 2) building and proving the "exhaustion" theorem for
    2.56 + * a datatype (I have called this theorem "nchotomy" for no good reason).
    2.57 + *
    2.58 + * It also brings all these together in the function "build_record", which
    2.59 + * is probably what will be used.
    2.60 + *
    2.61 + * Since these routines are required in order to support TFL, they have
    2.62 + * been written so they will compile "stand-alone", i.e., in Isabelle-HOL
    2.63 + * without any TFL code around.
    2.64 + *---------------------------------------------------------------------------*)
    2.65 +structure Dtype : Dtype_sig =
    2.66 +struct
    2.67 +
    2.68 +exception DTYPE_ERR of {func:string, mesg:string};
    2.69 +
    2.70 +(*---------------------------------------------------------------------------
    2.71 + * General support routines
    2.72 + *---------------------------------------------------------------------------*)
    2.73 +fun itlist f L base_value =
    2.74 +   let fun it [] = base_value
    2.75 +         | it (a::rst) = f a (it rst)
    2.76 +   in it L 
    2.77 +   end;
    2.78 +
    2.79 +fun end_itlist f =
    2.80 +let fun endit [] = raise DTYPE_ERR{func="end_itlist", mesg="list too short"}
    2.81 +      | endit alist = 
    2.82 +         let val (base::ralist) = rev alist
    2.83 +         in itlist f (rev ralist) base  end
    2.84 +in endit
    2.85 +end;
    2.86 +
    2.87 +fun unzip L = itlist (fn (x,y) => fn (l1,l2) =>((x::l1),(y::l2))) L ([],[]);
    2.88 +
    2.89 +
    2.90 +(*---------------------------------------------------------------------------
    2.91 + * Miscellaneous Syntax manipulation
    2.92 + *---------------------------------------------------------------------------*)
    2.93 +val mk_var = Free;
    2.94 +val mk_const = Const
    2.95 +fun mk_comb(Rator,Rand) = Rator $ Rand;
    2.96 +fun mk_abs(r as (Var((s,_),ty),_))  = Abs(s,ty,abstract_over r)
    2.97 +  | mk_abs(r as (Free(s,ty),_))     = Abs(s,ty,abstract_over r)
    2.98 +  | mk_abs _ = raise DTYPE_ERR{func="mk_abs", mesg="1st not a variable"};
    2.99 +
   2.100 +fun dest_var(Var((s,i),ty)) = (s,ty)
   2.101 +  | dest_var(Free(s,ty))    = (s,ty)
   2.102 +  | dest_var _ = raise DTYPE_ERR{func="dest_var", mesg="not a variable"};
   2.103 +
   2.104 +fun dest_const(Const p) = p
   2.105 +  | dest_const _ = raise DTYPE_ERR{func="dest_const", mesg="not a constant"};
   2.106 +
   2.107 +fun dest_comb(t1 $ t2) = (t1,t2)
   2.108 +  | dest_comb _ =  raise DTYPE_ERR{func = "dest_comb", mesg = "not a comb"};
   2.109 +val rand = #2 o dest_comb;
   2.110 +val rator = #1 o dest_comb;
   2.111 +
   2.112 +fun dest_abs(a as Abs(s,ty,M)) = 
   2.113 +     let val v = Free(s, ty)
   2.114 +      in (v, betapply (a,v)) end
   2.115 +  | dest_abs _ =  raise DTYPE_ERR{func="dest_abs", mesg="not an abstraction"};
   2.116 +
   2.117 +
   2.118 +val bool = Type("bool",[])
   2.119 +and prop = Type("prop",[]);
   2.120 +
   2.121 +fun mk_eq(lhs,rhs) = 
   2.122 +   let val ty = type_of lhs
   2.123 +       val c = mk_const("op =", ty --> ty --> bool)
   2.124 +   in list_comb(c,[lhs,rhs])
   2.125 +   end
   2.126 +
   2.127 +fun dest_eq(Const("op =",_) $ M $ N) = (M, N)
   2.128 +  | dest_eq _ = raise DTYPE_ERR{func="dest_eq", mesg="not an equality"};
   2.129 +
   2.130 +fun mk_disj(disj1,disj2) =
   2.131 +   let val c = Const("op |", bool --> bool --> bool)
   2.132 +   in list_comb(c,[disj1,disj2])
   2.133 +   end;
   2.134 +
   2.135 +fun mk_forall (r as (Bvar,_)) = 
   2.136 +  let val ty = type_of Bvar
   2.137 +      val c = Const("All", (ty --> bool) --> bool)
   2.138 +  in mk_comb(c, mk_abs r)
   2.139 +  end;
   2.140 +
   2.141 +fun mk_exists (r as (Bvar,_)) = 
   2.142 +  let val ty = type_of Bvar 
   2.143 +      val c = Const("Ex", (ty --> bool) --> bool)
   2.144 +  in mk_comb(c, mk_abs r)
   2.145 +  end;
   2.146 +
   2.147 +fun mk_prop (tm as Const("Trueprop",_) $ _) = tm
   2.148 +  | mk_prop tm = mk_comb(Const("Trueprop", bool --> prop),tm);
   2.149 +
   2.150 +fun drop_prop (Const("Trueprop",_) $ X) = X
   2.151 +  | drop_prop X = X;
   2.152 +
   2.153 +fun mk_all (r as (Bvar,_)) = mk_comb(all (type_of Bvar), mk_abs r);
   2.154 +fun list_mk_all(V,t) = itlist(fn v => fn b => mk_all(v,b)) V t;
   2.155 +fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists(v,b)) V t;
   2.156 +val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj(d1,tm))
   2.157 +
   2.158 +
   2.159 +fun dest_thm thm = 
   2.160 +   let val {prop,hyps,...} = rep_thm thm
   2.161 +   in (map drop_prop hyps, drop_prop prop)
   2.162 +   end;
   2.163 +
   2.164 +val concl = #2 o dest_thm;
   2.165 +
   2.166 +
   2.167 +(*---------------------------------------------------------------------------
   2.168 + * Names of all variables occurring in a term, including bound ones. These
   2.169 + * are added into the second argument.
   2.170 + *---------------------------------------------------------------------------*)
   2.171 +fun add_term_names tm =
   2.172 +let fun insert (x:string) = 
   2.173 +     let fun canfind[] = [x] 
   2.174 +           | canfind(alist as (y::rst)) = 
   2.175 +              if (x<y) then x::alist
   2.176 +              else if (x=y) then y::rst
   2.177 +              else y::canfind rst 
   2.178 +     in canfind end
   2.179 +    fun add (Free(s,_)) V = insert s V
   2.180 +      | add (Var((s,_),_)) V = insert s V
   2.181 +      | add (Abs(s,_,body)) V = add body (insert s V)
   2.182 +      | add (f$t) V = add t (add f V)
   2.183 +      | add _ V = V
   2.184 +in add tm
   2.185 +end;
   2.186 +
   2.187 +
   2.188 +(*---------------------------------------------------------------------------
   2.189 + * We need to make everything free, so that we can put the term into a
   2.190 + * goalstack, or submit it as an argument to prove_goalw_cterm.
   2.191 + *---------------------------------------------------------------------------*)
   2.192 +fun make_free_ty(Type(s,alist)) = Type(s,map make_free_ty alist)
   2.193 +  | make_free_ty(TVar((s,i),srt)) = TFree(s,srt)
   2.194 +  | make_free_ty x = x;
   2.195 +
   2.196 +fun make_free (Var((s,_),ty)) = Free(s,make_free_ty ty)
   2.197 +  | make_free (Abs(s,x,body)) = Abs(s,make_free_ty x, make_free body)
   2.198 +  | make_free (f$t) = (make_free f $ make_free t)
   2.199 +  | make_free (Const(s,ty)) = Const(s, make_free_ty ty)
   2.200 +  | make_free (Free(s,ty)) = Free(s, make_free_ty ty)
   2.201 +  | make_free b = b;
   2.202 +
   2.203 +
   2.204 +(*---------------------------------------------------------------------------
   2.205 + * Structure of case congruence theorem looks like this:
   2.206 + *
   2.207 + *    (M = M') 
   2.208 + *    ==> (!!x1,...,xk. (M' = C1 x1..xk) ==> (f1 x1..xk = f1' x1..xk)) 
   2.209 + *    ==> ... 
   2.210 + *    ==> (!!x1,...,xj. (M' = Cn x1..xj) ==> (fn x1..xj = fn' x1..xj)) 
   2.211 + *    ==>
   2.212 + *      (ty_case f1..fn M = ty_case f1'..fn' m')
   2.213 + *
   2.214 + * The input is the list of rules for the case construct for the type, i.e.,
   2.215 + * that found in the "ty.cases" field of a theory where datatype "ty" is
   2.216 + * defined.
   2.217 + *---------------------------------------------------------------------------*)
   2.218 +
   2.219 +fun build_case_cong sign case_rewrites =
   2.220 + let val clauses = map concl case_rewrites
   2.221 +     val clause1 = hd clauses
   2.222 +     val left = (#1 o dest_eq) clause1
   2.223 +     val ty = type_of ((#2 o dest_comb) left)
   2.224 +     val varnames = itlist add_term_names clauses []
   2.225 +     val M = variant varnames "M"
   2.226 +     val Mvar = Free(M, ty)
   2.227 +     val M' = variant (M::varnames) M
   2.228 +     val M'var = Free(M', ty)
   2.229 +     fun mk_clause clause =
   2.230 +       let val (lhs,rhs) = dest_eq clause
   2.231 +           val func = (#1 o strip_comb) rhs
   2.232 +           val (constr,xbar) = strip_comb(rand lhs)
   2.233 +           val (Name,Ty) = dest_var func
   2.234 +           val func'name = variant (M::M'::varnames) (Name^"a")
   2.235 +           val func' = mk_var(func'name,Ty)
   2.236 +       in (func', list_mk_all
   2.237 +                  (xbar, Logic.mk_implies
   2.238 +                         (mk_prop(mk_eq(M'var, list_comb(constr,xbar))),
   2.239 +                          mk_prop(mk_eq(list_comb(func, xbar),
   2.240 +                                        list_comb(func',xbar))))))   end
   2.241 +     val (funcs',clauses') = unzip (map mk_clause clauses)
   2.242 +     val lhsM = mk_comb(rator left, Mvar)
   2.243 +     val c = #1(strip_comb left)
   2.244 + in
   2.245 + cterm_of sign
   2.246 +  (make_free
   2.247 +   (Logic.list_implies(mk_prop(mk_eq(Mvar, M'var))::clauses',
   2.248 +                       mk_prop(mk_eq(lhsM, list_comb(c,(funcs'@[M'var])))))))
   2.249 + end
   2.250 + handle _ => raise DTYPE_ERR{func="build_case_cong",mesg="failed"};
   2.251 +
   2.252 +  
   2.253 +(*---------------------------------------------------------------------------
   2.254 + * Proves the result of "build_case_cong". 
   2.255 + *---------------------------------------------------------------------------*)
   2.256 +fun prove_case_cong nchotomy case_rewrites ctm =
   2.257 + let val {sign,t,...} = rep_cterm ctm
   2.258 +     val (Const("==>",_) $ tm $ _) = t
   2.259 +     val (Const("Trueprop",_) $ (Const("op =",_) $ _ $ Ma)) = tm
   2.260 +     val (Free(str,_)) = Ma
   2.261 +     val thm = prove_goalw_cterm[] ctm
   2.262 +              (fn prems =>
   2.263 +               [simp_tac (HOL_ss addsimps [hd prems]) 1,
   2.264 +                cut_inst_tac [("x",str)] (nchotomy RS spec) 1,
   2.265 +                REPEAT (SOMEGOAL (etac disjE ORELSE' etac exE)),
   2.266 +                ALLGOALS(asm_simp_tac(HOL_ss addsimps (prems@case_rewrites)))])
   2.267 + in standard (thm RS eq_reflection)
   2.268 + end
   2.269 + handle _ => raise DTYPE_ERR{func="prove_case_cong",mesg="failed"};
   2.270 +
   2.271 +
   2.272 +(*---------------------------------------------------------------------------
   2.273 + * Structure of exhaustion theorem looks like this:
   2.274 + *
   2.275 + *    !v. (EX y1..yi. v = C1 y1..yi) | ... | (EX y1..yj. v = Cn y1..yj)
   2.276 + *
   2.277 + * As for "build_case_cong", the input is the list of rules for the case 
   2.278 + * construct (the case "rewrites").
   2.279 + *---------------------------------------------------------------------------*)
   2.280 +fun build_nchotomy sign case_rewrites =
   2.281 + let val clauses = map concl case_rewrites
   2.282 +     val C_ybars = map (rand o #1 o dest_eq) clauses
   2.283 +     val varnames = itlist add_term_names C_ybars []
   2.284 +     val vname = variant varnames "v"
   2.285 +     val ty = type_of (hd C_ybars)
   2.286 +     val v = mk_var(vname,ty)
   2.287 +     fun mk_disj C_ybar =
   2.288 +       let val ybar = #2(strip_comb C_ybar)
   2.289 +       in list_mk_exists(ybar, mk_eq(v,C_ybar))
   2.290 +       end
   2.291 + in
   2.292 + cterm_of sign
   2.293 +   (make_free(mk_prop (mk_forall(v, list_mk_disj (map mk_disj C_ybars)))))
   2.294 + end
   2.295 + handle _ => raise DTYPE_ERR{func="build_nchotomy",mesg="failed"};
   2.296 +
   2.297 +
   2.298 +(*---------------------------------------------------------------------------
   2.299 + * Takes the induction tactic for the datatype, and the result from 
   2.300 + * "build_nchotomy" and proves the theorem.
   2.301 + *---------------------------------------------------------------------------*)
   2.302 +
   2.303 +fun prove_nchotomy induct_tac case_rewrites ctm =
   2.304 + let val {sign,t,...} = rep_cterm ctm
   2.305 +     val (Const ("Trueprop",_) $ g) = t
   2.306 +     val (Const ("All",_) $ Abs (v,_,_)) = g
   2.307 + in 
   2.308 + prove_goalw_cterm[] ctm
   2.309 +     (fn _ => [rtac allI 1,
   2.310 +               induct_tac v 1,
   2.311 +               ALLGOALS (simp_tac (HOL_ss addsimps case_rewrites)),
   2.312 +               ALLGOALS (fast_tac HOL_cs)])
   2.313 + end
   2.314 + handle _ => raise DTYPE_ERR {func="prove_nchotomy", mesg="failed"};
   2.315 +
   2.316 +
   2.317 +(*---------------------------------------------------------------------------
   2.318 + * Brings the preceeding functions together.
   2.319 + *---------------------------------------------------------------------------*)
   2.320 +fun case_thms sign case_rewrites induct_tac =
   2.321 +  let val nchotomy = prove_nchotomy induct_tac case_rewrites
   2.322 +                            (build_nchotomy sign case_rewrites)
   2.323 +      val cong = prove_case_cong nchotomy case_rewrites
   2.324 +                                 (build_case_cong sign case_rewrites)
   2.325 +  in {nchotomy=nchotomy, case_cong=cong}
   2.326 +  end;
   2.327 +
   2.328 +(*---------------------------------------------------------------------------
   2.329 + * Tests
   2.330 + *
   2.331 + * 
   2.332 +     Dtype.case_thms (sign_of List.thy) List.list.cases List.list.induct_tac;
   2.333 +     Dtype.case_thms (sign_of Prod.thy) [split] 
   2.334 +                     (fn s => res_inst_tac [("p",s)] PairE_lemma);
   2.335 +     Dtype.case_thms (sign_of Nat.thy) [nat_case_0, nat_case_Suc] nat_ind_tac;
   2.336 +
   2.337 + *
   2.338 + *---------------------------------------------------------------------------*)
   2.339 +
   2.340 +
   2.341 +(*---------------------------------------------------------------------------
   2.342 + * Given a theory and the name (and constructors) of a datatype declared in 
   2.343 + * an ancestor of that theory and an induction tactic for that datatype, 
   2.344 + * return the information that TFL needs. This should only be called once for
   2.345 + * a datatype, because "build_record" proves various facts, and thus is slow. 
   2.346 + * It fails on the datatype of pairs, which must be included for TFL to work. 
   2.347 + * The test shows how to  build the record for pairs.
   2.348 + *---------------------------------------------------------------------------*)
   2.349 +
   2.350 +local fun mk_rw th = (th RS eq_reflection) handle _ => th
   2.351 +      fun get_fact thy s = (get_axiom thy s handle _ => get_thm thy s)
   2.352 +in
   2.353 +fun build_record (thy,(ty,cl),itac) =
   2.354 + let val sign = sign_of thy
   2.355 +     fun const s = Const(s, the(Sign.const_type sign s))
   2.356 +     val case_rewrites = map (fn c => get_fact thy (ty^"_case_"^c)) cl
   2.357 +     val {nchotomy,case_cong} = case_thms sign case_rewrites itac
   2.358 + in
   2.359 +  (ty, {constructors = map(fn s => const s handle _ => const("op "^s)) cl,
   2.360 +        case_const = const (ty^"_case"),
   2.361 +        case_rewrites = map mk_rw case_rewrites,
   2.362 +        nchotomy = nchotomy,
   2.363 +        case_cong = case_cong})
   2.364 + end
   2.365 +end;
   2.366 +
   2.367 +
   2.368 +(*---------------------------------------------------------------------------
   2.369 + * Test
   2.370 + *
   2.371 + * 
   2.372 +    map Dtype.build_record 
   2.373 +          [(Nat.thy, ("nat",["0", "Suc"]), nat_ind_tac),
   2.374 +           (List.thy,("list",["[]", "#"]), List.list.induct_tac)]
   2.375 +    @
   2.376 +    [let val prod_case_thms = Dtype.case_thms (sign_of Prod.thy) [split] 
   2.377 +                                 (fn s => res_inst_tac [("p",s)] PairE_lemma)
   2.378 +         fun const s = Const(s, the(Sign.const_type (sign_of Prod.thy) s))
   2.379 +     in ("*", 
   2.380 +         {constructors = [const "Pair"],
   2.381 +            case_const = const "split",
   2.382 +         case_rewrites = [split RS eq_reflection],
   2.383 +             case_cong = #case_cong prod_case_thms,
   2.384 +              nchotomy = #nchotomy prod_case_thms}) end];
   2.385 +
   2.386 + *
   2.387 + *---------------------------------------------------------------------------*)
   2.388 +
   2.389 +end;
     3.1 --- a/src/HOL/thy_data.ML	Fri Apr 19 11:18:59 1996 +0200
     3.2 +++ b/src/HOL/thy_data.ML	Fri Apr 19 11:33:24 1996 +0200
     3.3 @@ -11,7 +11,35 @@
     3.4        None => empty_ss
     3.5      | Some (SS_DATA ss) => ss;
     3.6  
     3.7 -fun datatypes_of tname =
     3.8 -  case get_thydata tname "datatypes" of
     3.9 -      None => []
    3.10 -    | Some (DT_DATA ds) => ds;
    3.11 +
    3.12 +(** Information about datatypes **)
    3.13 +
    3.14 +(* Retrieve information for a specific datatype *)
    3.15 +fun datatype_info thy tname =
    3.16 +  case get_thydata (thyname_of_sign (sign_of thy)) "datatypes" of
    3.17 +      None => None
    3.18 +    | Some (DT_DATA ds) => assoc (ds, tname);
    3.19 +
    3.20 +fun match_info thy tname =
    3.21 +  case datatype_info thy tname of
    3.22 +      Some {case_const, constructors, ...} =>
    3.23 +        {case_const=case_const, constructors=constructors}
    3.24 +    | None => error ("No datatype \"" ^ tname ^ "\" defined in this theory.");
    3.25 +
    3.26 +fun induct_info thy tname =
    3.27 +  case datatype_info thy tname of
    3.28 +      Some {constructors, nchotomy, ...} =>
    3.29 +        {constructors=constructors, nchotomy=nchotomy}
    3.30 +    | None => error ("No datatype \"" ^ tname ^ "\" defined in this theory.");
    3.31 +
    3.32 +
    3.33 +(* Retrieve information for all datatypes defined in a theory and its
    3.34 +   ancestors *)
    3.35 +fun extract_info thy =
    3.36 +  let val (congs, rewrites) =
    3.37 +        case get_thydata (thyname_of_sign (sign_of thy)) "datatypes" of
    3.38 +            None => ([], [])
    3.39 +          | Some (DT_DATA ds) =>
    3.40 +              let val info = map snd ds
    3.41 +              in (map #case_cong info, flat (map #case_rewrites info)) end;
    3.42 +  in {case_congs = congs, case_rewrites = rewrites} end;
     4.1 --- a/src/HOL/thy_syntax.ML	Fri Apr 19 11:18:59 1996 +0200
     4.2 +++ b/src/HOL/thy_syntax.ML	Fri Apr 19 11:33:24 1996 +0200
     4.3 @@ -116,7 +116,7 @@
     4.4    fun mk_rules tname cons pre = " map (get_axiom thy) " ^
     4.5      mk_list (map (fn ((s, _), _) => quote (tname ^ pre ^ strip_quotes s)) cons);
     4.6  
     4.7 -  (*generate string for calling add_datatype*)
     4.8 +  (*generate string for calling add_datatype and build_record*)
     4.9    fun mk_params ((ts, tname), cons) =
    4.10     ("val (thy, " ^ tname ^ "_add_primrec) = Datatype.add_datatype\n"
    4.11      ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
    4.12 @@ -139,6 +139,9 @@
    4.13      \ val simps = inject @ distinct @ cases @ recs;\n\
    4.14      \ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\
    4.15      \end;\n\
    4.16 +    \val dummy = datatypes := Dtype.build_record (thy, " ^
    4.17 +      mk_pair (quote tname, mk_list (map (fst o fst) cons)) ^
    4.18 +      ", " ^ tname ^ ".induct_tac) :: (!datatypes);\n\
    4.19      \val dummy = Addsimps " ^ tname ^ ".simps;\n");
    4.20  
    4.21    (*parsers*)