1.1 --- a/src/Pure/Isar/obtain.ML	Tue Apr 03 19:24:11 2007 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Tue Apr 03 19:24:13 2007 +0200
     1.3 @@ -82,7 +82,7 @@
     1.4      val _ = ObjectLogic.is_judgment thy (Thm.concl_of thm) orelse
     1.5        error "Conclusion in obtained context must be object-logic judgment";
     1.6  
     1.7 -    val ((_, [thm']), ctxt') = Variable.import true [thm] fix_ctxt;
     1.8 +    val ((_, [thm']), ctxt') = Variable.import_thms true [thm] fix_ctxt;
     1.9      val prems = Drule.strip_imp_prems (#prop (Thm.crep_thm thm'));
    1.10    in
    1.11      ((Drule.implies_elim_list thm' (map Thm.assume prems)
    1.12 @@ -198,7 +198,7 @@
    1.13        | SOME th => check_result ctxt thesis (MetaSimplifier.norm_hhf (Goal.conclude th)));
    1.14  
    1.15      val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
    1.16 -    val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
    1.17 +    val ((_, [rule']), ctxt') = Variable.import_thms false [closed_rule] ctxt;
    1.18      val obtain_rule = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule';
    1.19      val ((params, stmt), fix_ctxt) = Variable.focus (Thm.cprem_of obtain_rule 1) ctxt';
    1.20      val (prems, ctxt'') =
    1.21 @@ -251,7 +251,7 @@
    1.22        |> Thm.forall_intr (cert (Free thesis_var))
    1.23        |> Thm.instantiate (instT, []);
    1.24  
    1.25 -    val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt;
    1.26 +    val ((_, rule' :: terms'), ctxt') = Variable.import_thms false (closed_rule :: terms) ctxt;
    1.27      val vars' =
    1.28        map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~
    1.29        (map snd vars @ replicate (length ys) NoSyn);