ftuong
/
citadelle-devel
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

continue 7096030e62

This commit is contained in:
Frédéric Tuong 2018-06-27 11:26:18 -04:00
parent f588f4ac40
commit 1b56f09fcc
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/compiler_generic/isabelle_d_atomic/src/HOL/Tools/inductive_realizer.ML
View File

@ -246,7 +246,7 @@ fun add_dummies f [] _ thy =
thy
|> f (map snd dts)
|-> (fn dtinfo => pair (map fst dts, SOME dtinfo))
handle BNF_FP_Util.EMPTY_DATATYPE name' =>
handle Old_Datatype_Aux.Datatype_Empty name' =>
let
val name = Long_Name.base_name name';
val dname = singleton (Name.variant_list used) "Dummy";
@ -315,10 +315,10 @@ fun add_ind_realizer rsets intrs induct raw_induct elims vs thy =
||> Extraction.add_typeof_eqns_i ty_eqs
||> Extraction.add_realizes_eqns_i rlz_eqs;
val dt_names = these some_dt_names;
val case_thms = map (#case_rewrites o BNF_LFP_Compat.the_info thy2 []) dt_names;
val case_thms = map (#case_rewrites o Old_Datatype_Data.the_info thy2) dt_names;
val rec_thms =
if null dt_names then []
else #rec_rewrites (BNF_LFP_Compat.the_info thy2 [] (hd dt_names));
else #rec_rewrites (Old_Datatype_Data.the_info thy2 (hd dt_names));
val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) rec_thms);
val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>