src/HOL/Code_Evaluation.thy
changeset 58334 7553a1bcecb7
parent 58310 91ea607a34d8
child 58350 919149921e46
     1.1 --- a/src/HOL/Code_Evaluation.thy	Sat Sep 13 18:08:45 2014 +0200
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Sun Sep 14 22:59:30 2014 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  subsubsection {* Terms and class @{text term_of} *}
     1.6  
     1.7 -datatype "term" = dummy_term
     1.8 +datatype (plugins only: code) "term" = dummy_term
     1.9  
    1.10  definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
    1.11    "Const _ _ = dummy_term"
    1.12 @@ -113,7 +113,7 @@
    1.13  
    1.14  end
    1.15  
    1.16 -declare [[code drop: rec_term case_term size_term "size :: term \<Rightarrow> _" "HOL.equal :: term \<Rightarrow> _"
    1.17 +declare [[code drop: rec_term case_term "HOL.equal :: term \<Rightarrow> _"
    1.18    "term_of :: typerep \<Rightarrow> _" "term_of :: term \<Rightarrow> _" "term_of :: String.literal \<Rightarrow> _"
    1.19    "term_of :: _ Predicate.pred \<Rightarrow> term" "term_of :: _ Predicate.seq \<Rightarrow> term"]]
    1.20