Thm.no_prems;
authorwenzelm
Tue Sep 21 17:29:46 1999 +0200 (1999-09-21)
changeset 756326ca52846865
parent 7562 8519d5019309
child 7564 90455fa8cebe
Thm.no_prems;
src/HOL/ex/meson.ML
     1.1 --- a/src/HOL/ex/meson.ML	Tue Sep 21 17:29:00 1999 +0200
     1.2 +++ b/src/HOL/ex/meson.ML	Tue Sep 21 17:29:46 1999 +0200
     1.3 @@ -437,7 +437,7 @@
     1.4    having only one eq_assume_tac speeds it up!*)
     1.5  fun prolog_step_tac' horns = 
     1.6      let val (horn0s, hornps) = (*0 subgoals vs 1 or more*)
     1.7 -            take_prefix (fn rl => nprems_of rl=0) horns
     1.8 +            take_prefix Thm.no_prems horns
     1.9          val nrtac = net_resolve_tac horns
    1.10      in  fn i => eq_assume_tac i ORELSE
    1.11                  match_tac horn0s i ORELSE  (*no backtracking if unit MATCHES*)