--- a/IsaMakefile	Mon Dec 07 14:35:45 2009 +0100
+++ b/IsaMakefile	Mon Dec 07 14:37:10 2009 +0100
@@ -3,9 +3,8 @@
 
 default: Quot
 images: 
-test: Quot
 
-all: images test
+all: Quot
 
 
 ## global settings
@@ -16,13 +15,12 @@
 
 USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -d pdf  ## -D generated
 
-
 ## Quot
 
 Quot: $(LOG)/HOL-Quot.gz
 
 $(LOG)/HOL-Quot.gz: Quot/ROOT.ML Quot/*.thy
-	@$(USEDIR) HOL Quot
+	@$(USEDIR) HOL-Nominal Quot
 
 
 ## clean

--- a/Quot/Examples/IntEx.thy	Mon Dec 07 14:35:45 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Mon Dec 07 14:37:10 2009 +0100
@@ -274,3 +274,5 @@
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* lambda_prs_tac  @{context} 1 *})
 sorry
+
+end
\ No newline at end of file

--- a/Quot/Examples/IntEx2.thy	Mon Dec 07 14:35:45 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Mon Dec 07 14:37:10 2009 +0100
@@ -434,3 +434,5 @@
 lemmas normalize_bin_simps =
   Bit0_Pls Bit1_Min
 *)
+
+end
\ No newline at end of file

--- a/Quot/Examples/LamEx.thy	Mon Dec 07 14:35:45 2009 +0100
+++ b/Quot/Examples/LamEx.thy	Mon Dec 07 14:37:10 2009 +0100
@@ -250,3 +250,4 @@
   apply(simp add: var_supp)
   done
 
+end
\ No newline at end of file

--- a/Quot/ROOT.ML	Mon Dec 07 14:35:45 2009 +0100
+++ b/Quot/ROOT.ML	Mon Dec 07 14:37:10 2009 +0100
@@ -1,4 +1,8 @@
-(*
-  no_document use_thys ["This_Theory1", "This_Theory2"];
-  use_thys ["That_Theory1", "That_Theory2", "That_Theory3"];
-*)
+no_document use_thys 
+   ["QuotMain",
+    "Examples/Fset",
+    "Examples/IntEx",
+    "Examples/IntEx2",
+    "Examples/LFex",
+    "Examples/LamEx"];
+