src/HOL/Code_Evaluation.thy

   "App _ _ = dummy_term"
 
 definition Abs :: "String.literal \<Rightarrow> typerep \<Rightarrow> term \<Rightarrow> term" where
   "Abs _ _ _ = dummy_term"
 
-code_datatype Const App Abs
+definition Free :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
+  "Free _ _ = dummy_term"
+
+code_datatype Const App Abs Free
 
 class term_of = typerep +
   fixes term_of :: "'a \<Rightarrow> term"
 
 lemma term_of_anything: "term_of x \<equiv> t"

   by (subst term_of_anything) rule 
 
 code_type "term"
   (Eval "Term.term")
 
-code_const Const and App and Abs
-  (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))" and "Term.Abs/ ((_), (_), (_))")
+code_const Const and App and Abs and Free
+  (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))" and "Term.Abs/ ((_), (_), (_))"
+     and "Term.Free/ ((_), (_))")
 
 code_const "term_of \<Colon> String.literal \<Rightarrow> term"
   (Eval "HOLogic.mk'_literal")
 
 code_reserved Eval HOLogic

 code_const "tracing :: String.literal => 'a => 'a"
   (Eval "Code'_Evaluation.tracing")
 
 
 hide_const dummy_term valapp
-hide_const (open) Const App Abs termify valtermify term_of term_of_num_semiring term_of_num_ring tracing
-
-end
+hide_const (open) Const App Abs Free termify valtermify term_of term_of_num_semiring term_of_num_ring tracing
+
+end