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