src/HOL/BNF_LFP.thy
changeset 55575 a5e33e18fb5c
parent 55571 a6153343c44f
child 55770 f2cf7f92c9ac
--- a/src/HOL/BNF_LFP.thy	Wed Feb 19 08:34:32 2014 +0100
+++ b/src/HOL/BNF_LFP.thy	Wed Feb 19 08:34:33 2014 +0100
@@ -13,8 +13,7 @@
 imports BNF_FP_Base
 keywords
   "datatype_new" :: thy_decl and
-  "datatype_compat" :: thy_decl and
-  "primrec" :: thy_decl
+  "datatype_compat" :: thy_decl
 begin
 
 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
@@ -241,7 +240,6 @@
 ML_file "Tools/BNF/bnf_lfp_tactics.ML"
 ML_file "Tools/BNF/bnf_lfp.ML"
 ML_file "Tools/BNF/bnf_lfp_compat.ML"
-ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
 ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
 
 hide_fact (open) id_transfer