# 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 \ term \ term" where "App _ _ = dummy_term" -code_datatype Const App +definition Abs :: "String.literal \ typerep \ term \ term" where + "Abs _ _ _ = dummy_term" + +code_datatype Const App Abs class term_of = typerep + fixes term_of :: "'a \ 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 \ String.literal \ 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