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