src/Pure/Isar/obtain.ML
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 []