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/Tools/Predicate_Compile/predicate_compile_core.ML
changeset 38795 848be46708dc
parent 38558 32ad17fe2b9c
child 38797 abe92b33ac9f 
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -524,7 +524,7 @@
 
 fun dest_conjunct_prem th =
   case HOLogic.dest_Trueprop (prop_of th) of
-    (Const (@{const_name "op &"}, _) $ t $ t') =>
+    (Const (@{const_name HOL.conj}, _) $ t $ t') =>
       dest_conjunct_prem (th RS @{thm conjunct1})
         @ dest_conjunct_prem (th RS @{thm conjunct2})
     | _ => [th]
isabelle