# HG changeset patch
# User paulson
# Date 921059039 -3600
# Node ID f523a7c91c37508a7a6681723272cbc2294c7650
# Parent  7e4bffaa2a3ea94d56648159e7ba928c93e989a0
allow meta_outer to do nothing

diff -r 7e4bffaa2a3e -r f523a7c91c37 TFL/post.sml
--- a/TFL/post.sml	Wed Mar 10 10:42:57 1999 +0100
+++ b/TFL/post.sml	Wed Mar 10 10:43:59 1999 +0100
@@ -175,8 +175,9 @@
 (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
 val meta_outer = 
     curry_rule o standard o 
-    rule_by_tactic (REPEAT_FIRST (resolve_tac [allI, impI, conjI]
-				  ORELSE' etac conjE));
+    rule_by_tactic (REPEAT 
+		    (FIRSTGOAL (resolve_tac [allI, impI, conjI]
+				ORELSE' etac conjE)));
 
 (*Strip off the outer !P*)
 val spec'= read_instantiate [("x","P::?'b=>bool")] spec;