# HG changeset patch
# User wenzelm
# Date 1192556756 -7200
# Node ID e6e0ee56a67282894b2f49e12d816c490151861c
# Parent  d8d8bac48031a0d32f5fd0ab304dba1d5eef9c22
apply_wrappers: perhaps_apply/loop;

diff -r d8d8bac48031 -r e6e0ee56a672 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Oct 16 19:45:54 2007 +0200
+++ b/src/Pure/theory.ML	Tue Oct 16 19:45:56 2007 +0200
@@ -83,26 +83,12 @@
 
 
 
-(** theory wrappers **)
+(** datatype thy **)
 
 type wrapper = (theory -> theory option) * stamp;
 
 fun apply_wrappers (wrappers: wrapper list) =
-  let
-    fun app [] res = res
-      | app ((f, _) :: fs) (changed, thy) =
-          (case f thy of
-            NONE => app fs (changed, thy)
-          | SOME thy' => app fs (true, thy'));
-    fun app_fixpoint thy =
-      (case app wrappers (false, thy) of
-        (false, _) => thy
-      | (true, thy') => app_fixpoint thy');
-  in app_fixpoint end;
-
-
-
-(** datatype thy **)
+  perhaps (perhaps_loop (perhaps_apply (map fst wrappers)));
 
 datatype thy = Thy of
  {axioms: term NameSpace.table,