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*)