streamlined code setup for fake terms
authorhaftmann
Mon Jun 05 15:59:45 2017 +0200 (2017-06-05)
changeset 6601303002d10bf1d
parent 66012 59bf29d2b3a1
child 66014 2f45f4abf0a9
streamlined code setup for fake terms
src/HOL/Code_Evaluation.thy
     1.1 --- a/src/HOL/Code_Evaluation.thy	Mon Jun 05 15:59:45 2017 +0200
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Mon Jun 05 15:59:45 2017 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  subsubsection \<open>Terms and class \<open>term_of\<close>\<close>
     1.6  
     1.7 -datatype (plugins only: code extraction) "term" = dummy_term
     1.8 +datatype (plugins only: extraction) "term" = dummy_term
     1.9  
    1.10  definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
    1.11    "Const _ _ = dummy_term"
    1.12 @@ -115,7 +115,7 @@
    1.13  
    1.14  end
    1.15  
    1.16 -declare [[code drop: rec_term case_term "HOL.equal :: term \<Rightarrow> _"
    1.17 +declare [[code drop: rec_term case_term
    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  
    1.21 @@ -172,4 +172,3 @@
    1.22  hide_const (open) Const App Abs Free termify valtermify term_of tracing
    1.23  
    1.24  end
    1.25 -