# HG changeset patch
# User nipkow
# Date 1201710963 -3600
# Node ID 31115576b8586eb223bb147a5bd5005a63d346ee
# Parent  f9d1bf2fc59c38c3699e37490ba22ff826cc5e9e
commented stuff out

diff -r f9d1bf2fc59c -r 31115576b858 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"