src/HOL/Statespace/state_space.ML

--- a/src/HOL/Statespace/state_space.ML	Thu Mar 12 15:54:19 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML	Thu Mar 12 15:54:58 2009 +0100
@@ -419,7 +419,7 @@
         val expr = ([(suffix valuetypesN name, 
                      (("",false),Expression.Positional (map SOME pars)))],[]);
       in
-        prove_interpretation_in (ALLGOALS o solve_tac o Assumption.prems_of)
+        prove_interpretation_in (ALLGOALS o solve_tac o Assumption.all_prems_of)
           (suffix valuetypesN name, expr) thy
       end;