src/HOL/Library/rewrite.ML
changeset 60108 d7fe3e0aca85
parent 60088 0a064330a885
child 60109 22389d4cdd6b
     1.1 --- a/src/HOL/Library/rewrite.ML	Thu Apr 16 15:55:55 2015 +0200
     1.2 +++ b/src/HOL/Library/rewrite.ML	Fri Apr 17 10:49:57 2015 +0200
     1.3 @@ -406,6 +406,8 @@
     1.4  
     1.5          fun append_default [] = [Concl, In]
     1.6            | append_default (ps as Term _ :: _) = Concl :: In :: ps
     1.7 +          | append_default [For x, In] = [For x, Concl, In]
     1.8 +          | append_default (For x :: (ps as In :: Term _:: _)) = For x :: Concl :: ps
     1.9            | append_default ps = ps
    1.10  
    1.11        in Scan.repeat sep_atom >> (flat #> rev #> append_default) end