1.1 --- a/src/HOL/BNF/BNF_FP_Base.thy	Wed Sep 18 16:44:19 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_FP_Base.thy	Wed Sep 18 17:36:47 2013 +0200
     1.3 @@ -13,11 +13,6 @@
     1.4  imports BNF_Comp BNF_Ctr_Sugar
     1.5  begin
     1.6  
     1.7 -definition code_unspec :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a" where
     1.8 -[code del]: "code_unspec f = f ()"
     1.9 -
    1.10 -code_abort code_unspec
    1.11 -
    1.12  lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
    1.13  by auto
    1.14