# HG changeset patch
# User haftmann
# Date 1496671185 -7200
# Node ID 03002d10bf1dd5acfdbe6fbb7cd46c6c06a0fb18
# Parent  59bf29d2b3a142d5a00a14401c337cb2492fdf26
streamlined code setup for fake terms

diff -r 59bf29d2b3a1 -r 03002d10bf1d src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Mon Jun 05 15:59:45 2017 +0200
+++ b/src/HOL/Code_Evaluation.thy	Mon Jun 05 15:59:45 2017 +0200
@@ -13,7 +13,7 @@
 
 subsubsection \<open>Terms and class \<open>term_of\<close>\<close>
 
-datatype (plugins only: code extraction) "term" = dummy_term
+datatype (plugins only: extraction) "term" = dummy_term
 
 definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
   "Const _ _ = dummy_term"
@@ -115,7 +115,7 @@
 
 end
 
-declare [[code drop: rec_term case_term "HOL.equal :: term \<Rightarrow> _"
+declare [[code drop: rec_term case_term
   "term_of :: typerep \<Rightarrow> _" "term_of :: term \<Rightarrow> _" "term_of :: String.literal \<Rightarrow> _"
   "term_of :: _ Predicate.pred \<Rightarrow> term" "term_of :: _ Predicate.seq \<Rightarrow> term"]]
 
@@ -172,4 +172,3 @@
 hide_const (open) Const App Abs Free termify valtermify term_of tracing
 
 end
-