diff -r cbc38731d42f -r 0fbed69ff081 src/Sequents/modal.ML
--- a/src/Sequents/modal.ML	Tue Mar 03 19:08:04 2015 +0100
+++ b/src/Sequents/modal.ML	Wed Mar 04 19:53:18 2015 +0100
@@ -69,12 +69,12 @@
 
 fun UPTOGOAL n tf = let fun tac i = if i<n then all_tac
                                     else tf(i) THEN tac(i-1)
-                    in fn st => tac (nprems_of st) st end;
+                    in fn st => tac (Thm.nprems_of st) st end;
 
 (* Depth first search bounded by d *)
 fun solven_tac ctxt d n st = st |>
  (if d < 0 then no_tac
-  else if nprems_of st = 0 then all_tac
+  else if Thm.nprems_of st = 0 then all_tac
   else (DETERM(fres_safe_tac ctxt n) THEN UPTOGOAL n (solven_tac ctxt d)) ORELSE
            ((fres_unsafe_tac ctxt n  THEN UPTOGOAL n (solven_tac ctxt d)) APPEND
              (fres_bound_tac ctxt n  THEN UPTOGOAL n (solven_tac ctxt (d - 1)))));