--- a/src/HOL/Code_Evaluation.thy Thu May 26 00:20:28 2011 +0200
+++ b/src/HOL/Code_Evaluation.thy Thu May 26 09:42:02 2011 +0200
@@ -24,7 +24,10 @@
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"
@@ -127,8 +130,9 @@
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")
@@ -197,6 +201,6 @@
hide_const dummy_term valapp
-hide_const (open) Const App Abs termify valtermify term_of term_of_num_semiring term_of_num_ring tracing
+hide_const (open) Const App Abs Free termify valtermify term_of term_of_num_semiring term_of_num_ring tracing
end