--- 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
--- 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;
--- 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 **)
--- 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 *)
--- 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;