# HG changeset patch
# User bulwahn
# Date 1290418917 -3600
# Node ID 6b137c96df07525ff9434669910ef44c456ac6c9
# Parent  58c36606a74de58f9f716e72b54faf8e24ec8c8c
adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict

diff -r 58c36606a74d -r 6b137c96df07 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Mon Nov 22 10:41:56 2010 +0100
+++ b/src/HOL/Code_Evaluation.thy	Mon Nov 22 10:41:57 2010 +0100
@@ -21,7 +21,10 @@
 definition App :: "term \<Rightarrow> term \<Rightarrow> term" where
   "App _ _ = dummy_term"
 
-code_datatype Const App
+definition Abs :: "String.literal \<Rightarrow> typerep \<Rightarrow> term \<Rightarrow> term" where
+  "Abs _ _ _ = dummy_term"
+
+code_datatype Const App Abs
 
 class term_of = typerep +
   fixes term_of :: "'a \<Rightarrow> term"
@@ -124,8 +127,8 @@
 code_type "term"
   (Eval "Term.term")
 
-code_const Const and App
-  (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))")
+code_const Const and App and Abs
+  (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))" and "Term.Abs/ ((_), (_), (_))")
 
 code_const "term_of \<Colon> String.literal \<Rightarrow> term"
   (Eval "HOLogic.mk'_literal")
@@ -184,7 +187,7 @@
   (Eval "Code'_Evaluation.tracing")
 
 
-hide_const dummy_term App valapp
-hide_const (open) Const termify valtermify term_of term_of_num tracing
+hide_const dummy_term valapp
+hide_const (open) Const App Abs termify valtermify term_of term_of_num tracing
 
 end