# HG changeset patch
# User blanchet
# Date 1410210258 -7200
# Node ID a701907d621eaa0cee6fc60a1ff3c795b7d02f75
# Parent  17200800a5538d6885524834c72a1f2e8e57628f
ported old Nominal to use new datatypes

diff -r 17200800a553 -r a701907d621e src/HOL/Nominal/Examples/SOS.thy
--- a/src/HOL/Nominal/Examples/SOS.thy	Mon Sep 08 20:42:52 2014 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy	Mon Sep 08 23:04:18 2014 +0200
@@ -11,7 +11,7 @@
 (* Christian Urban.                                       *)
 
 theory SOS
-  imports "Nominal"
+  imports "../Nominal"
 begin
 
 atom_decl name
diff -r 17200800a553 -r a701907d621e src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Mon Sep 08 20:42:52 2014 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Mon Sep 08 23:04:18 2014 +0200
@@ -18,10 +18,14 @@
   swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x"
 
 (* a "private" copy of the option type used in the abstraction function *)
-datatype 'a noption = nSome 'a | nNone
+datatype_new 'a noption = nSome 'a | nNone
+
+datatype_compat noption
 
 (* a "private" copy of the product type used in the nominal induct method *)
-datatype ('a, 'b) nprod = nPair 'a 'b
+datatype_new ('a, 'b) nprod = nPair 'a 'b
+
+datatype_compat nprod
 
 (* an auxiliary constant for the decision procedure involving *) 
 (* permutations (to avoid loops when using perm-compositions)  *)
diff -r 17200800a553 -r a701907d621e src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Mon Sep 08 20:42:52 2014 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Sep 08 23:04:18 2014 +0200
@@ -100,10 +100,9 @@
     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) =
-                Old_Datatype.add_datatype Old_Datatype_Aux.default_config [dt] thy;
+              val (dt_names, thy1) = BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Unfold_Nesting [dt] thy;
             
-              val injects = maps (#inject o Old_Datatype_Data.the_info thy1) dt_names;
+              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,[])
               val ak_sign = Sign.intern_const thy1 ak 
               
diff -r 17200800a553 -r a701907d621e src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Mon Sep 08 20:42:52 2014 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Sep 08 23:04:18 2014 +0200
@@ -200,9 +200,9 @@
 
     val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
 
-    val (full_new_type_names',thy1) = Old_Datatype.add_datatype config dts'' thy;
+    val (full_new_type_names',thy1) = BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Unfold_Nesting dts'' thy;
 
-    val {descr, induct, ...} = Old_Datatype_Data.the_info thy1 (hd full_new_type_names');
+    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);
 
     val big_name = space_implode "_" new_type_names;