src/Pure/Isar/obtain.ML
changeset 20218 be3bfb0699ba
parent 20201 24b49cbd438b
child 20224 9c40a144ee0e
     1.1 --- a/src/Pure/Isar/obtain.ML	Wed Jul 26 19:23:04 2006 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Wed Jul 26 19:37:41 2006 +0200
     1.3 @@ -209,7 +209,7 @@
     1.4      val instT =
     1.5        fold (Term.add_tvarsT o #2) params []
     1.6        |> map (TVar #> (fn T => (certT T, certT (norm_type T))));
     1.7 -    val (rule' :: terms', ctxt') =
     1.8 +    val ((_, rule' :: terms'), ctxt') =
     1.9        Variable.import false (Thm.instantiate (instT, []) rule :: terms) ctxt;
    1.10  
    1.11      val vars' =