# HG changeset patch
# User wenzelm
# Date 937927786 -7200
# Node ID 26ca52846865649c9fcc0a64f37571e1e9c53dff
# Parent  8519d50193090b573ceffba21d2982693a7cb8bd
Thm.no_prems;

diff -r 8519d5019309 -r 26ca52846865 src/HOL/ex/meson.ML
--- 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*)