src/HOL/ex/NBE.thy

--- a/src/HOL/ex/NBE.thy	Wed Jan 30 17:34:21 2008 +0100
+++ b/src/HOL/ex/NBE.thy	Wed Jan 30 17:36:03 2008 +0100
@@ -4,18 +4,21 @@
 *)
 header {* Normalization by Evaluation *}
 
-theory NBE imports Main Executable_Set begin
+theory NBE imports Main (*Executable_Set*) begin
 
 ML"Syntax.ambiguity_level := 1000000"
 
 declare Let_def[simp]
 
-consts_code undefined ("(raise Match)")
-
-(*typedecl const_name*)
 types lam_var_name = nat
       ml_var_name = nat
-      const_name = nat
+
+typedecl const_name
+(*
+types const_name = nat
+
+consts_code undefined ("(raise Match)")
+*)
 
 datatype ml = (* rep of universal datatype *)
           C const_name "ml list" | V lam_var_name "ml list"