--- a/src/HOL/Nominal/Examples/Type_Preservation.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Nominal/Examples/Type_Preservation.thy Thu Sep 11 18:54:36 2014 +0200
@@ -1,5 +1,5 @@
theory Type_Preservation
- imports Nominal
+ imports "../Nominal"
begin
text {*
--- a/src/HOL/Nominal/nominal_atoms.ML Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Thu Sep 11 18:54:36 2014 +0200
@@ -100,7 +100,7 @@
val (_,thy1) =
fold_map (fn ak => fn thy =>
let val dt = ((Binding.name ak, [], NoSyn), [(Binding.name ak, [@{typ nat}], NoSyn)])
- val (dt_names, thy1) = BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Unfold_Nesting [dt] thy;
+ val (dt_names, thy1) = BNF_LFP_Compat.add_datatype_dead BNF_LFP_Compat.Unfold_Nesting [dt] thy;
val injects = maps (#inject o BNF_LFP_Compat.the_info thy1 BNF_LFP_Compat.Unfold_Nesting) dt_names;
val ak_type = Type (Sign.intern_type thy1 ak,[])
--- a/src/HOL/Nominal/nominal_datatype.ML Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Thu Sep 11 18:54:36 2014 +0200
@@ -200,7 +200,7 @@
val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
- val (full_new_type_names',thy1) = BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Unfold_Nesting dts'' thy;
+ val (full_new_type_names',thy1) = BNF_LFP_Compat.add_datatype_dead BNF_LFP_Compat.Unfold_Nesting dts'' thy;
val {descr, induct, ...} = BNF_LFP_Compat.the_info thy1 BNF_LFP_Compat.Unfold_Nesting (hd full_new_type_names');
fun nth_dtyp i = Old_Datatype_Aux.typ_of_dtyp descr (Old_Datatype_Aux.DtRec i);
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Sep 11 18:54:36 2014 +0200
@@ -27,6 +27,8 @@
val datatype_compat_cmd: string list -> local_theory -> local_theory
val add_datatype: nesting_preference -> Old_Datatype_Aux.spec list -> theory ->
string list * theory
+ val add_datatype_dead: nesting_preference -> Old_Datatype_Aux.spec list -> theory ->
+ string list * theory
val add_primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
local_theory -> (term list * thm list) * local_theory
val add_primrec_global: (binding * typ option * mixfix) list ->
@@ -495,11 +497,12 @@
datatype_compat fpT_names lthy
end;
-fun add_datatype nesting_pref old_specs thy =
+fun gen_add_datatype live nesting_pref old_specs thy =
let
val fpT_names = map (Sign.full_name thy o #1 o fst) old_specs;
- fun new_type_args_of (s, S) = (SOME Binding.empty, (TFree (s, @{sort type}), S));
+ fun new_type_args_of (s, S) =
+ (if live then SOME Binding.empty else NONE, (TFree (s, @{sort type}), S));
fun new_ctr_spec_of (b, Ts, mx) = (((Binding.empty, b), map (pair Binding.empty) Ts), mx);
fun new_spec_of ((b, old_tyargs, mx), old_ctr_specs) =
@@ -514,6 +517,9 @@
|> nesting_pref = Unfold_Nesting ? perhaps (try (datatype_compat_global fpT_names)))
end;
+val add_datatype = gen_add_datatype true;
+val add_datatype_dead = gen_add_datatype false;
+
val add_primrec = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec;
val add_primrec_global = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec_global;
val add_primrec_overloaded = apfst (apsnd flat) oooo BNF_LFP_Rec_Sugar.add_primrec_overloaded;