Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Statespace/state_fun.ML
changeset 38795 848be46708dc
parent 38715 6513ea67d95d
child 38864 4abe644fcea5 
--- a/src/HOL/Statespace/state_fun.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Statespace/state_fun.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -53,7 +53,7 @@
 val lazy_conj_simproc =
   Simplifier.simproc_global @{theory HOL} "lazy_conj_simp" ["P & Q"]
     (fn thy => fn ss => fn t =>
-      (case t of (Const (@{const_name "op &"},_)$P$Q) => 
+      (case t of (Const (@{const_name HOL.conj},_)$P$Q) => 
          let
             val P_P' = Simplifier.rewrite ss (cterm_of thy P);
             val P' = P_P' |> prop_of |> Logic.dest_equals |> #2
isabelle