# HG changeset patch
# User haftmann
# Date 1162560161 -3600
# Node ID 95142d816793c231abcd6642028cef27eab06859
# Parent  c8cc6b68759fe27a32161afc858e4b4b04e4f377
added particular test for partially applied case constants

diff -r c8cc6b68759f -r 95142d816793 src/HOL/ex/Codegenerator.thy
--- a/src/HOL/ex/Codegenerator.thy	Fri Nov 03 14:22:40 2006 +0100
+++ b/src/HOL/ex/Codegenerator.thy	Fri Nov 03 14:22:41 2006 +0100
@@ -5,7 +5,7 @@
 header {* Test and Examples for code generator *}
 
 theory Codegenerator
-imports Main (*"~/projects/codegen/thy/CodegenSetup"*) Records
+imports Main Records
 begin
 
 subsection {* booleans *}
@@ -99,6 +99,9 @@
 definition
   "case_let x = (let (y, z) = x in case y of () => z)"
 
+definition
+  "base_case f = f list_case"
+
 subsection {* heavy usage of names *}
 
 definition
@@ -158,6 +161,7 @@
 code_gen
   remdups
   "distinct"
+  filter
 code_gen
   foo1 foo3
 code_gen
@@ -165,7 +169,7 @@
 code_gen
   f g h
 code_gen
-  apply_tower Codegenerator.keywords shadow
+  apply_tower Codegenerator.keywords shadow base_case
 code_gen
   abs_let nested_let case_let
 code_gen "0::int" "1::int"