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/ex/SVC_Oracle.thy
changeset 52131 366fa32ee2a3
parent 48891 c0eafbd55de3
child 56245 84fc7dfa3cd4 
--- a/src/HOL/ex/SVC_Oracle.thy	Fri May 24 16:42:57 2013 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy	Fri May 24 17:00:46 2013 +0200
@@ -57,7 +57,7 @@
         case t of
             Free _  => t  (*but not existing Vars, lest the names clash*)
           | Bound _ => t
-          | _ => (case AList.lookup Pattern.aeconv (!pairs) t of
+          | _ => (case AList.lookup Envir.aeconv (!pairs) t of
                       SOME v => v
                     | NONE   => insert t)
     (*abstraction of a numeric literal*)
isabelle