# HG changeset patch # User blanchet # Date 1409594268 -7200 # Node ID 6dcee1f6ea6531f03bd4bd2a8f986c49793175ea # Parent 1abeda3c3bc275cae17211fb6a6d6a1d37356214 ported TFL to mixture of old and new datatypes diff -r 1abeda3c3bc2 -r 6dcee1f6ea65 src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Mon Sep 01 19:28:00 2014 +0200 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Mon Sep 01 19:57:48 2014 +0200 @@ -144,7 +144,7 @@ | @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct) | _ => raise CTERM ("no equation", [ct])) - fun get_constrs thy (Type (n, _)) = these (Old_Datatype_Data.get_constrs thy n) + fun get_constrs thy (Type (n, _)) = these (BNF_LFP_Compat.get_constrs thy n) | get_constrs _ _ = [] fun is_constr thy (n, T) = diff -r 1abeda3c3bc2 -r 6dcee1f6ea65 src/HOL/Tools/TFL/casesplit.ML --- a/src/HOL/Tools/TFL/casesplit.ML Mon Sep 01 19:28:00 2014 +0200 +++ b/src/HOL/Tools/TFL/casesplit.ML Mon Sep 01 19:57:48 2014 +0200 @@ -24,7 +24,7 @@ Type(ty_str, _) => ty_str | TFree(s,_) => error ("Free type: " ^ s) | TVar((s,i),_) => error ("Free variable: " ^ s) - val {induct, ...} = Old_Datatype_Data.the_info thy ty_str + val {induct, ...} = BNF_LFP_Compat.the_info thy BNF_LFP_Compat.Keep_Nesting ty_str in cases_thm_of_induct_thm induct end; diff -r 1abeda3c3bc2 -r 6dcee1f6ea65 src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Mon Sep 01 19:28:00 2014 +0200 +++ b/src/HOL/Tools/TFL/tfl.ML Mon Sep 01 19:57:48 2014 +0200 @@ -435,7 +435,7 @@ put_simpset HOL_basic_ss ctxt addsimps case_rewrites |> fold (Simplifier.add_cong o #case_cong_weak o snd) - (Symtab.dest (Old_Datatype_Data.get_all theory)) + (Symtab.dest (BNF_LFP_Compat.get_all theory BNF_LFP_Compat.Keep_Nesting)) val corollaries' = map (Simplifier.simplify case_simpset) corollaries val extract = Rules.CONTEXT_REWRITE_RULE (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs) diff -r 1abeda3c3bc2 -r 6dcee1f6ea65 src/HOL/Tools/TFL/thry.ML --- a/src/HOL/Tools/TFL/thry.ML Mon Sep 01 19:28:00 2014 +0200 +++ b/src/HOL/Tools/TFL/thry.ML Mon Sep 01 19:57:48 2014 +0200 @@ -58,20 +58,20 @@ *---------------------------------------------------------------------------*) fun match_info thy dtco = - case (Old_Datatype_Data.get_info thy dtco, - Old_Datatype_Data.get_constrs thy dtco) of - (SOME { case_name, ... }, SOME constructors) => + case (BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Keep_Nesting dtco, + BNF_LFP_Compat.get_constrs thy dtco) of + (SOME {case_name, ... }, SOME constructors) => SOME {case_const = Const (case_name, Sign.the_const_type thy case_name), constructors = map Const constructors} | _ => NONE; -fun induct_info thy dtco = case Old_Datatype_Data.get_info thy dtco of +fun induct_info thy dtco = case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Keep_Nesting dtco of NONE => NONE | SOME {nchotomy, ...} => SOME {nchotomy = nchotomy, - constructors = (map Const o the o Old_Datatype_Data.get_constrs thy) dtco}; + constructors = (map Const o the o BNF_LFP_Compat.get_constrs thy) dtco}; fun extract_info thy = - let val infos = map snd (Symtab.dest (Old_Datatype_Data.get_all thy)) + let val infos = map snd (Symtab.dest (BNF_LFP_Compat.get_all thy BNF_LFP_Compat.Keep_Nesting)) in {case_congs = map (mk_meta_eq o #case_cong) infos, case_rewrites = maps (map mk_meta_eq o #case_rewrites) infos} end;