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