changeset 19906 | c23a0e65b285 |
parent 19897 | fe661eb3b0e7 |
child 19978 | df19a7876183 |
--- a/src/Pure/Isar/obtain.ML Sat Jun 17 19:37:46 2006 +0200 +++ b/src/Pure/Isar/obtain.ML Sat Jun 17 19:37:47 2006 +0200 @@ -200,7 +200,7 @@ val xs = map (apsnd norm_type) vars; val ys = map (apsnd norm_type) (Library.drop (m, params)); - val ys' = map Syntax.internal (Term.variantlist (map fst ys, map fst xs)) ~~ map #2 ys; + val ys' = map Term.internal (Term.variantlist (map fst ys, map fst xs)) ~~ map #2 ys; val instT = fold (Term.add_tvarsT o #2) params []