thread the right local theory through + reenable parallel proofs for previously problematic theories
authorblanchet
Wed Oct 03 22:07:26 2012 +0200 (2012-10-03)
changeset 49693393d7242adaf
parent 49692 a8a3b82b37f8
child 49694 bdec6330acc4
thread the right local theory through + reenable parallel proofs for previously problematic theories
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/ROOT
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Oct 03 21:46:52 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Oct 03 22:07:26 2012 +0200
     1.3 @@ -640,7 +640,7 @@
     1.4  
     1.5              val [foldx, recx] = map (mk_rec_like lfp As Cs o Morphism.term phi) csts;
     1.6            in
     1.7 -            ((foldx, recx, fold_def, rec_def), lthy)
     1.8 +            ((foldx, recx, fold_def, rec_def), lthy')
     1.9            end;
    1.10  
    1.11          fun define_unfold_corec no_defs_lthy =
    1.12 @@ -698,7 +698,7 @@
    1.13  
    1.14              val [unfold, corec] = map (mk_rec_like lfp As Cs o Morphism.term phi) csts;
    1.15            in
    1.16 -            ((unfold, corec, unfold_def, corec_def), lthy)
    1.17 +            ((unfold, corec, unfold_def, corec_def), lthy')
    1.18            end;
    1.19  
    1.20          val define_rec_likes = if lfp then define_fold_rec else define_unfold_corec;
     2.1 --- a/src/HOL/ROOT	Wed Oct 03 21:46:52 2012 +0200
     2.2 +++ b/src/HOL/ROOT	Wed Oct 03 22:07:26 2012 +0200
     2.3 @@ -631,7 +631,7 @@
     2.4      "Infinite_Derivation_Trees/Gram_Lang"
     2.5      "Infinite_Derivation_Trees/Parallel"
     2.6      Stream
     2.7 -  theories [parallel_proofs = 0, condition = ISABELLE_FULL_TEST]
     2.8 +  theories [condition = ISABELLE_FULL_TEST]
     2.9      Misc_Codata
    2.10      Misc_Data
    2.11