# 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*)