thread the right local theory through + reenable parallel proofs for previously problematic theories

--- 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;

--- 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