# HG changeset patch
# User haftmann
# Date 1204214096 -3600
# Node ID 0cc3ff184282a648c87801d5c344a8efaf80ac69
# Parent  8262ec0e8782f088c506d73a2abf2e32d3d91689
import all 'special code' types

diff -r 8262ec0e8782 -r 0cc3ff184282 src/HOL/Library/RType.thy
--- a/src/HOL/Library/RType.thy	Thu Feb 28 16:50:52 2008 +0100
+++ b/src/HOL/Library/RType.thy	Thu Feb 28 16:54:56 2008 +0100
@@ -6,7 +6,7 @@
 header {* Reflecting Pure types into HOL *}
 
 theory RType
-imports Main Code_Message
+imports Main Code_Message Code_Index (* import all 'special code' types *)
 begin
 
 datatype "rtype" = RType message_string "rtype list"