src/HOL/Transfer.thy
changeset 59276 d207455817e8
parent 59275 77cd4992edcd
child 59514 509caf5edfa6
--- a/src/HOL/Transfer.thy	Fri Dec 19 14:06:13 2014 +0100
+++ b/src/HOL/Transfer.thy	Mon Jan 05 06:56:15 2015 +0100
@@ -371,12 +371,6 @@
 ML_file "Tools/Transfer/transfer_bnf.ML"
 ML_file "Tools/BNF/bnf_fp_rec_sugar_transfer.ML"
 
-ML {*
-val _ = Theory.setup (BNF_LFP_Rec_Sugar.primrec_interpretation
-  BNF_FP_Rec_Sugar_Transfer.primrec_transfer_pluginN
-  BNF_FP_Rec_Sugar_Transfer.primrec_transfer_interpretation)
-*}
-
 declare pred_fun_def [simp]
 declare rel_fun_eq [relator_eq]