Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/obtain.ML
changeset 20218 be3bfb0699ba
parent 20201 24b49cbd438b
child 20224 9c40a144ee0e 
--- 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' =
isabelle