src/Pure/Isar/obtain.ML

 
     val _ = eliminate_term fix_ctxt xs (Thm.full_prop_of thm);
     val _ = ObjectLogic.is_judgment thy (Thm.concl_of thm) orelse
       error "Conclusion in obtained context must be object-logic judgment";
 
-    val ((_, [thm']), ctxt') = Variable.import_thms true [thm] fix_ctxt;
+    val ((_, [thm']), ctxt') = Variable.import true [thm] fix_ctxt;
     val prems = Drule.strip_imp_prems (#prop (Thm.crep_thm thm'));
   in
     ((Drule.implies_elim_list thm' (map Thm.assume prems)
         |> Drule.implies_intr_list (map Drule.norm_hhf_cterm As)
         |> Drule.forall_intr_list xs)

       (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) (Goal.init (cert thesis)) of
         NONE => raise THM ("Obtain.result: tactic failed", 0, facts)
       | SOME th => check_result ctxt thesis (MetaSimplifier.norm_hhf (Goal.conclude th)));
 
     val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
-    val ((_, [rule']), ctxt') = Variable.import_thms false [closed_rule] ctxt;
+    val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
     val obtain_rule = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule';
     val ((params, stmt), fix_ctxt) = Variable.focus (Thm.cprem_of obtain_rule 1) ctxt';
     val (prems, ctxt'') =
       Assumption.add_assms (obtain_export fix_ctxt obtain_rule params)
         (Drule.strip_imp_prems stmt) fix_ctxt;

       |> map (TVar #> (fn T => (certT T, certT (norm_type T))));
     val closed_rule = rule
       |> Thm.forall_intr (cert (Free thesis_var))
       |> Thm.instantiate (instT, []);
 
-    val ((_, rule' :: terms'), ctxt') = Variable.import_thms false (closed_rule :: terms) ctxt;
+    val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt;
     val vars' =
       map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~
       (map snd vars @ replicate (length ys) NoSyn);
     val rule'' = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule';
   in ((vars', rule''), ctxt') end;