# HG changeset patch
# User blanchet
# Date 1410454476 -7200
# Node ID 055afb5f7df81447873126a14c11dce9f14d78b0
# Parent  30ab8289f0e14bffe8d7f5f0ba828e45c5eaed3a
speed up old Nominal by killing type variables

diff -r 30ab8289f0e1 -r 055afb5f7df8 src/HOL/Nominal/Examples/Type_Preservation.thy
--- 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 {*
diff -r 30ab8289f0e1 -r 055afb5f7df8 src/HOL/Nominal/nominal_atoms.ML
--- 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,[])
diff -r 30ab8289f0e1 -r 055afb5f7df8 src/HOL/Nominal/nominal_datatype.ML
--- 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);
diff -r 30ab8289f0e1 -r 055afb5f7df8 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- 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;