src/HOL/Tools/datatype_rep_proofs.ML
changeset 11628 e57a6e51715e
parent 11539 0f17da240450
child 11806 e1fd22a657ae
equal deleted inserted replaced
11627:abf9cda4a4d2 11628:e57a6e51715e
   173         ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names));
   173         ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names));
   174 
   174 
   175     val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
   175     val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
   176       setmp InductivePackage.quiet_mode (!quiet_mode)
   176       setmp InductivePackage.quiet_mode (!quiet_mode)
   177         (InductivePackage.add_inductive_i false true big_rec_name false true false
   177         (InductivePackage.add_inductive_i false true big_rec_name false true false
   178            consts [] (map (fn x => (("", x), [])) intr_ts) [Funs_mono] []) thy1;
   178            consts (map (fn x => (("", x), [])) intr_ts) [Funs_mono] []) thy1;
   179 
   179 
   180     (********************************* typedef ********************************)
   180     (********************************* typedef ********************************)
   181 
   181 
   182     val thy3 = add_path flat_names big_name (foldl (fn (thy, ((((name, mx), tvs), c), name')) =>
   182     val thy3 = add_path flat_names big_name (foldl (fn (thy, ((((name, mx), tvs), c), name')) =>
   183       setmp TypedefPackage.quiet_mode true
   183       setmp TypedefPackage.quiet_mode true