Logic.is_all;
authorwenzelm
Mon Jun 23 23:45:45 2008 +0200 (2008-06-23)
changeset 2733294790a9620c3
parent 27331 5c66afff695e
child 27333 7095f775131a
Logic.is_all;
src/Pure/conv.ML
src/Pure/old_goals.ML
     1.1 --- a/src/Pure/conv.ML	Mon Jun 23 23:45:44 2008 +0200
     1.2 +++ b/src/Pure/conv.ML	Mon Jun 23 23:45:45 2008 +0200
     1.3 @@ -133,7 +133,7 @@
     1.4  
     1.5  (*rewrite B in !!x1 ... xn. B*)
     1.6  fun params_conv n cv ctxt ct =
     1.7 -  if n <> 0 andalso can Logic.dest_all (Thm.term_of ct)
     1.8 +  if n <> 0 andalso Logic.is_all (Thm.term_of ct)
     1.9    then arg_conv (abs_conv (params_conv (n - 1) cv o #2) ctxt) ct
    1.10    else cv ctxt ct;
    1.11  
     2.1 --- a/src/Pure/old_goals.ML	Mon Jun 23 23:45:44 2008 +0200
     2.2 +++ b/src/Pure/old_goals.ML	Mon Jun 23 23:45:45 2008 +0200
     2.3 @@ -155,7 +155,7 @@
     2.4        val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg;
     2.5        val (As, B) = Logic.strip_horn horn;
     2.6        val atoms = atomic andalso
     2.7 -            forall (fn t => not (can Logic.dest_implies t orelse can Logic.dest_all t)) As;
     2.8 +            forall (fn t => not (can Logic.dest_implies t orelse Logic.is_all t)) As;
     2.9        val (As,B) = if atoms then ([],horn) else (As,B);
    2.10        val cAs = map (cterm_of thy) As;
    2.11        val prems = map (rewrite_rule rths o Thm.forall_elim_vars 0 o Thm.assume) cAs;