# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1349345423 -3600
# Node ID 995d47b09ab422aefba6b52b1da2536f0143dfc2
# Parent  93e7c1d8cc5c9bfa11f4f643f5388a622e2e6105
removed fork_mono flag

diff -r 93e7c1d8cc5c -r 995d47b09ab4 IsaMakefile
--- a/IsaMakefile	Tue Aug 28 16:48:07 2012 +0100
+++ b/IsaMakefile	Thu Oct 04 11:10:23 2012 +0100
@@ -30,7 +30,7 @@
 $(LOG)/HOL-Nominal2-tests.gz: Nominal/ROOT.ML Nominal/*.thy
 	@$(USEDIR) HOL Nominal
 	@$(USEDIR) HOL Tutorial
-	@$(USEDIR) HOL Nominal/Ex/CPS
+#	@$(USEDIR) HOL Nominal/Ex/CPS
 
 ## ESOP Paper
 
diff -r 93e7c1d8cc5c -r 995d47b09ab4 Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Tue Aug 28 16:48:07 2012 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Thu Oct 04 11:10:23 2012 +0100
@@ -250,7 +250,7 @@
 
     val (alpha_info, lthy') = Inductive.add_inductive_i
        {quiet_mode = true, verbose = false, alt_name = Binding.empty,
-        coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
+        coind = false, no_elim = false, no_ind = false, skip_mono = false}
          all_alpha_names [] all_alpha_intros [] lthy
 
     val all_alpha_trms_loc = #preds alpha_info;
diff -r 93e7c1d8cc5c -r 995d47b09ab4 Nominal/nominal_function_core.ML
--- a/Nominal/nominal_function_core.ML	Tue Aug 28 16:48:07 2012 +0100
+++ b/Nominal/nominal_function_core.ML	Thu Oct 04 11:10:23 2012 +0100
@@ -602,8 +602,7 @@
             coind = false,
             no_elim = false,
             no_ind = false,
-            skip_mono = true,
-            fork_mono = false}
+            skip_mono = true}
           [binding] (* relation *)
           [] (* no parameters *)
           (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)