# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1268835211 -3600
# Node ID dc7b049d90727e8f9b84655376d3d782c34ac3aa
# Parent  2ca8e43b53c576f4b1907bec97762e4d7cd4c2a1
made paper to compile

diff -r 2ca8e43b53c5 -r dc7b049d9072 IsaMakefile
--- a/IsaMakefile	Wed Mar 17 15:13:03 2010 +0100
+++ b/IsaMakefile	Wed Mar 17 15:13:31 2010 +0100
@@ -27,7 +27,7 @@
 
 $(LOG)/HOL-Nominal2-Paper.gz: Paper/ROOT.ML Paper/document/root.tex Paper/*.thy
 	@$(USEDIR) -D generated HOL Paper
-	$(ISATOOL) document -o pdf  Paper/generated
+	$(ISABELLE_TOOL) document -o pdf  Paper/generated
 	@cp Paper/document.pdf paper.pdf
 
 ## clean
diff -r 2ca8e43b53c5 -r dc7b049d9072 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Wed Mar 17 15:13:03 2010 +0100
+++ b/Nominal/Parser.thy	Wed Mar 17 15:13:31 2010 +0100
@@ -276,14 +276,14 @@
 *}
 
 (* These 2 are critical, we don't know how to do it in term5 *)
-ML {* val cheat_fv_rsp = ref true *}
-ML {* val cheat_const_rsp = ref true *} (* For alpha_bn 0 and alpha_bn_rsp *)
+ML {* val cheat_fv_rsp = Unsynchronized.ref true *}
+ML {* val cheat_const_rsp = Unsynchronized.ref true *} (* For alpha_bn 0 and alpha_bn_rsp *)
 
-ML {* val cheat_equivp = ref true *}
+ML {* val cheat_equivp = Unsynchronized.ref true *}
 
 (* Fixes for these 2 are known *)
-ML {* val cheat_fv_eqvt = ref true *} (* The tactic works, building the goal needs fixing *)
-ML {* val cheat_alpha_eqvt = ref true *} (* The tactic works, building the goal needs fixing *)
+ML {* val cheat_fv_eqvt = Unsynchronized.ref true *} (* The tactic works, building the goal needs fixing *)
+ML {* val cheat_alpha_eqvt = Unsynchronized.ref true *} (* The tactic works, building the goal needs fixing *)
 
 
 ML {*
@@ -520,7 +520,7 @@
 *}
 
 ML {*
-val recursive = ref false
+val recursive = Unsynchronized.ref false
 *}
 
 ML {*
diff -r 2ca8e43b53c5 -r dc7b049d9072 Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Mar 17 15:13:03 2010 +0100
+++ b/Paper/Paper.thy	Wed Mar 17 15:13:31 2010 +0100
@@ -11,6 +11,9 @@
 
 *}
 
+
+
+
 (*<*)
 end
 (*>*)
\ No newline at end of file
diff -r 2ca8e43b53c5 -r dc7b049d9072 Paper/ROOT.ML
--- a/Paper/ROOT.ML	Wed Mar 17 15:13:03 2010 +0100
+++ b/Paper/ROOT.ML	Wed Mar 17 15:13:31 2010 +0100
@@ -1,3 +1,3 @@
-no_document use_thys ["../Quot/QuotMain"];
-
+quick_and_dirty := true;
+no_document use_thys ["../Nominal/Test"];
 use_thys ["Paper"];
\ No newline at end of file
diff -r 2ca8e43b53c5 -r dc7b049d9072 Paper/document/root.tex
--- a/Paper/document/root.tex	Wed Mar 17 15:13:03 2010 +0100
+++ b/Paper/document/root.tex	Wed Mar 17 15:13:31 2010 +0100
@@ -1,4 +1,5 @@
-\documentstyle[epsf]{acmconf}
+\documentclass{article}
+%%\documentclass[epsf]{acmconf}
 \usepackage{isabelle,isabellesym}
 
 % further packages required for unusual symbols (see also