allow meta_outer to do nothing
authorpaulson
Wed Mar 10 10:43:59 1999 +0100 (1999-03-10)
changeset 6336f523a7c91c37
parent 6335 7e4bffaa2a3e
child 6337 150182bcb7da
allow meta_outer to do nothing
TFL/post.sml
     1.1 --- a/TFL/post.sml	Wed Mar 10 10:42:57 1999 +0100
     1.2 +++ b/TFL/post.sml	Wed Mar 10 10:43:59 1999 +0100
     1.3 @@ -175,8 +175,9 @@
     1.4  (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
     1.5  val meta_outer = 
     1.6      curry_rule o standard o 
     1.7 -    rule_by_tactic (REPEAT_FIRST (resolve_tac [allI, impI, conjI]
     1.8 -				  ORELSE' etac conjE));
     1.9 +    rule_by_tactic (REPEAT 
    1.10 +		    (FIRSTGOAL (resolve_tac [allI, impI, conjI]
    1.11 +				ORELSE' etac conjE)));
    1.12  
    1.13  (*Strip off the outer !P*)
    1.14  val spec'= read_instantiate [("x","P::?'b=>bool")] spec;