diff -r 25b068a99d2b -r be3bfb0699ba src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Wed Jul 26 19:23:04 2006 +0200
+++ b/src/Pure/Isar/obtain.ML	Wed Jul 26 19:37:41 2006 +0200
@@ -209,7 +209,7 @@
     val instT =
       fold (Term.add_tvarsT o #2) params []
       |> map (TVar #> (fn T => (certT T, certT (norm_type T))));
-    val (rule' :: terms', ctxt') =
+    val ((_, rule' :: terms'), ctxt') =
       Variable.import false (Thm.instantiate (instT, []) rule :: terms) ctxt;
 
     val vars' =