# HG changeset patch
# User blanchet
# Date 1349294846 -7200
# Node ID 393d7242adaf4c0ac3eb703033d1e29951fbf0ad
# Parent  a8a3b82b37f8a08d341311e24fee9e39d9a95b6e
thread the right local theory through + reenable parallel proofs for previously problematic theories

diff -r a8a3b82b37f8 -r 393d7242adaf src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Oct 03 21:46:52 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Oct 03 22:07:26 2012 +0200
@@ -640,7 +640,7 @@
 
             val [foldx, recx] = map (mk_rec_like lfp As Cs o Morphism.term phi) csts;
           in
-            ((foldx, recx, fold_def, rec_def), lthy)
+            ((foldx, recx, fold_def, rec_def), lthy')
           end;
 
         fun define_unfold_corec no_defs_lthy =
@@ -698,7 +698,7 @@
 
             val [unfold, corec] = map (mk_rec_like lfp As Cs o Morphism.term phi) csts;
           in
-            ((unfold, corec, unfold_def, corec_def), lthy)
+            ((unfold, corec, unfold_def, corec_def), lthy')
           end;
 
         val define_rec_likes = if lfp then define_fold_rec else define_unfold_corec;
diff -r a8a3b82b37f8 -r 393d7242adaf src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Oct 03 21:46:52 2012 +0200
+++ b/src/HOL/ROOT	Wed Oct 03 22:07:26 2012 +0200
@@ -631,7 +631,7 @@
     "Infinite_Derivation_Trees/Gram_Lang"
     "Infinite_Derivation_Trees/Parallel"
     Stream
-  theories [parallel_proofs = 0, condition = ISABELLE_FULL_TEST]
+  theories [condition = ISABELLE_FULL_TEST]
     Misc_Codata
     Misc_Data