apply_wrappers: perhaps_apply/loop;
authorwenzelm
Tue Oct 16 19:45:56 2007 +0200 (2007-10-16)
changeset 25059e6e0ee56a672
parent 25058 d8d8bac48031
child 25060 17c313217998
apply_wrappers: perhaps_apply/loop;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Tue Oct 16 19:45:54 2007 +0200
     1.2 +++ b/src/Pure/theory.ML	Tue Oct 16 19:45:56 2007 +0200
     1.3 @@ -83,26 +83,12 @@
     1.4  
     1.5  
     1.6  
     1.7 -(** theory wrappers **)
     1.8 +(** datatype thy **)
     1.9  
    1.10  type wrapper = (theory -> theory option) * stamp;
    1.11  
    1.12  fun apply_wrappers (wrappers: wrapper list) =
    1.13 -  let
    1.14 -    fun app [] res = res
    1.15 -      | app ((f, _) :: fs) (changed, thy) =
    1.16 -          (case f thy of
    1.17 -            NONE => app fs (changed, thy)
    1.18 -          | SOME thy' => app fs (true, thy'));
    1.19 -    fun app_fixpoint thy =
    1.20 -      (case app wrappers (false, thy) of
    1.21 -        (false, _) => thy
    1.22 -      | (true, thy') => app_fixpoint thy');
    1.23 -  in app_fixpoint end;
    1.24 -
    1.25 -
    1.26 -
    1.27 -(** datatype thy **)
    1.28 +  perhaps (perhaps_loop (perhaps_apply (map fst wrappers)));
    1.29  
    1.30  datatype thy = Thy of
    1.31   {axioms: term NameSpace.table,