Thm.no_prems;

--- a/src/HOL/ex/meson.ML	Tue Sep 21 17:29:00 1999 +0200
+++ b/src/HOL/ex/meson.ML	Tue Sep 21 17:29:46 1999 +0200
@@ -437,7 +437,7 @@
   having only one eq_assume_tac speeds it up!*)
 fun prolog_step_tac' horns = 
     let val (horn0s, hornps) = (*0 subgoals vs 1 or more*)
-            take_prefix (fn rl => nprems_of rl=0) horns
+            take_prefix Thm.no_prems horns
         val nrtac = net_resolve_tac horns
     in  fn i => eq_assume_tac i ORELSE
                 match_tac horn0s i ORELSE  (*no backtracking if unit MATCHES*)