# HG changeset patch
# User blanchet
# Date 1410177837 -7200
# Node ID f5144942a83aa30a9bcc3d2f0d9424eab6be01fd
# Parent  622daea5b925f82c8be77f8f8740304679b72ea0
use compatibility layer

diff -r 622daea5b925 -r f5144942a83a src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Mon Sep 08 14:03:46 2014 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Sep 08 14:03:57 2014 +0200
@@ -191,7 +191,7 @@
         val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
       in
         thy' |>
-        Old_Primrec.add_primrec_global
+        BNF_LFP_Compat.add_primrec_global
           [(Binding.name swap_name, SOME swapT, NoSyn)]
           [(Attrib.empty_binding, def1)] ||>
         Sign.parent_path ||>>
@@ -225,7 +225,7 @@
                     Const (swap_name, swapT) $ x $ (prm $ xs $ a)));
       in
         thy' |>
-        Old_Primrec.add_primrec_global
+        BNF_LFP_Compat.add_primrec_global
           [(Binding.name prm_name, SOME prmT, NoSyn)]
           [(Attrib.empty_binding, def1), (Attrib.empty_binding, def2)] ||>
         Sign.parent_path
diff -r 622daea5b925 -r f5144942a83a src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Mon Sep 08 14:03:46 2014 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Sep 08 14:03:57 2014 +0200
@@ -254,7 +254,7 @@
       end) descr;
 
     val (perm_simps, thy2) =
-      Old_Primrec.add_primrec_overloaded
+      BNF_LFP_Compat.add_primrec_overloaded
         (map (fn (s, sT) => (s, sT, false))
            (List.take (perm_names' ~~ perm_names_types, length new_type_names)))
         (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs thy1;
diff -r 622daea5b925 -r f5144942a83a src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Sep 08 14:03:46 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Sep 08 14:03:57 2014 +0200
@@ -39,9 +39,9 @@
 
 (* basics *)
 
-val exhaustive_plugin = "exhaustive"
-val bounded_forall_plugin = "bounded_forall"
-val full_exhaustive_plugin = "full_exhaustive"
+val exhaustive_plugin = "quickcheck_exhaustive"
+val bounded_forall_plugin = "quickcheck_bounded_forall"
+val full_exhaustive_plugin = "quickcheck_full_exhaustive"
 
 
 (** dynamic options **)
diff -r 622daea5b925 -r f5144942a83a src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Sep 08 14:03:46 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Sep 08 14:03:57 2014 +0200
@@ -23,7 +23,7 @@
 structure Narrowing_Generators : NARROWING_GENERATORS =
 struct
 
-val narrowing_plugin = "narrowing"
+val narrowing_plugin = "quickcheck_narrowing"
 
 (* configurations *)
 
diff -r 622daea5b925 -r f5144942a83a src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Sep 08 14:03:46 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Sep 08 14:03:57 2014 +0200
@@ -25,7 +25,7 @@
 structure Random_Generators : RANDOM_GENERATORS =
 struct
 
-val random_plugin = "random";
+val random_plugin = "quickcheck_random";
 
 (** abstract syntax **)
 
@@ -100,7 +100,7 @@
     val eqs0 = [subst_v @{term "0::natural"} eq,
       subst_v (@{const Code_Numeral.Suc} $ t_k) eq];
     val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
-    val ((_, (_, eqs2)), lthy') = Old_Primrec.add_primrec_simple
+    val ((_, (_, eqs2)), lthy') = BNF_LFP_Compat.add_primrec_simple
       [((Binding.conceal (Binding.name random_aux), T), NoSyn)] eqs1 lthy;
     val cT_random_aux = inst pt_random_aux;
     val cT_rhs = inst pt_rhs;