changeset 38786 | e46e7a9cb622 |
parent 38549 | d0385f2764d8 |
child 41229 | d797baa3d57c |
--- a/src/HOL/TLA/Intensional.thy Thu Aug 26 13:44:50 2010 +0200 +++ b/src/HOL/TLA/Intensional.thy Thu Aug 26 20:51:17 2010 +0200 @@ -279,7 +279,7 @@ fun hflatten t = case (concl_of t) of - Const _ $ (Const (@{const_name "op -->"}, _) $ _ $ _) => hflatten (t RS mp) + Const _ $ (Const (@{const_name HOL.implies}, _) $ _ $ _) => hflatten (t RS mp) | _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t in hflatten t