# HG changeset patch
# User bulwahn
# Date 1306395722 -7200
# Node ID 5b9e16259341d61072491b0a472b5e073cb9801c
# Parent  6b41a075251f252907547adef060e2fc4347bc53
extending terms of Code_Evaluation by Free to allow partial terms

diff -r 6b41a075251f -r 5b9e16259341 src/HOL/Code_Evaluation.thy
--- 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