# HG changeset patch
# User wenzelm
# Date 1559674173 -7200
# Node ID aa7c49651f4ec93b2f13766993f9b0f2a518d3ef
# Parent  9bf04a8f211fd6314f3e2b911b1b0aed56c582e0
tuned;

diff -r 9bf04a8f211f -r aa7c49651f4e src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Jun 04 20:01:02 2019 +0200
+++ b/src/HOL/HOL.thy	Tue Jun 04 20:49:33 2019 +0200
@@ -1251,7 +1251,7 @@
       else
         let (*Norbert Schirmer's case*)
           val t = Thm.term_of ct;
-          val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
+          val (t', ctxt') = yield_singleton (Variable.import_terms false) t ctxt;
         in
           Option.map (hd o Variable.export ctxt' ctxt o single)
             (case t' of Const (\<^const_name>\<open>Let\<close>,_) $ x $ f => (* x and f are already in normal form *)
diff -r 9bf04a8f211f -r aa7c49651f4e src/HOL/Library/Cancellation/cancel.ML
--- a/src/HOL/Library/Cancellation/cancel.ML	Tue Jun 04 20:01:02 2019 +0200
+++ b/src/HOL/Library/Cancellation/cancel.ML	Tue Jun 04 20:49:33 2019 +0200
@@ -47,7 +47,7 @@
 fun proc ctxt ct =
   let
     val t = Thm.term_of ct
-    val ([t'], ctxt') = Variable.import_terms true [t] ctxt
+    val (t', ctxt') = yield_singleton (Variable.import_terms true) t ctxt
     val pre_simplified_ct = Simplifier.full_rewrite (clear_simpset ctxt addsimps
       Named_Theorems.get ctxt \<^named_theorems>\<open>cancelation_simproc_pre\<close> addsimprocs
       [\<^simproc>\<open>NO_MATCH\<close>]) (Thm.cterm_of ctxt t');
diff -r 9bf04a8f211f -r aa7c49651f4e src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Tue Jun 04 20:01:02 2019 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Tue Jun 04 20:49:33 2019 +0200
@@ -162,7 +162,8 @@
           commas_quote xs));
     val induct_cases = map (fst o fst) (fst (Rule_Cases.get (the
       (Induct.lookup_inductP ctxt (hd names)))));
-    val ([raw_induct'], ctxt') = Variable.import_terms false [Thm.prop_of raw_induct] ctxt;
+    val (raw_induct', ctxt') = ctxt
+      |> yield_singleton (Variable.import_terms false) (Thm.prop_of raw_induct);
     val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>
       HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb);
     val ps = map (fst o snd) concls;
diff -r 9bf04a8f211f -r aa7c49651f4e src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Tue Jun 04 20:01:02 2019 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Tue Jun 04 20:49:33 2019 +0200
@@ -169,7 +169,8 @@
       (Induct.lookup_inductP ctxt (hd names)))));
     val induct_cases' = if null induct_cases then replicate (length intrs) ""
       else induct_cases;
-    val ([raw_induct'], ctxt') = Variable.import_terms false [Thm.prop_of raw_induct] ctxt;
+    val (raw_induct', ctxt') = ctxt
+      |> yield_singleton (Variable.import_terms false) (Thm.prop_of raw_induct);
     val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>
       HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb);
     val ps = map (fst o snd) concls;
diff -r 9bf04a8f211f -r aa7c49651f4e src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jun 04 20:01:02 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jun 04 20:49:33 2019 +0200
@@ -737,7 +737,7 @@
         | _ =>
           if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
           else t |> Envir.eta_contract |> do_lambdas ctxt Ts)
-      val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
+      val (t, ctxt') = yield_singleton (Variable.import_terms true) t ctxt
     in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end
 
 fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
diff -r 9bf04a8f211f -r aa7c49651f4e src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Tue Jun 04 20:01:02 2019 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Tue Jun 04 20:49:33 2019 +0200
@@ -320,7 +320,7 @@
   (case Item_Net.content (get_functions ctxt) of
     [] => NONE
   | (t, _) :: _ =>
-      let val ([t'], ctxt') = Variable.import_terms true [t] ctxt
+      let val (t', ctxt') = yield_singleton (Variable.import_terms true) t ctxt
       in import_function_data t' ctxt' end)
 
 
diff -r 9bf04a8f211f -r aa7c49651f4e src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Tue Jun 04 20:01:02 2019 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue Jun 04 20:49:33 2019 +0200
@@ -346,8 +346,8 @@
                             | _ => false) fully_skolemized_t then
           let
             val (fully_skolemized_ct, ctxt) =
-              Variable.import_terms true [fully_skolemized_t] ctxt
-              |>> the_single |>> Thm.cterm_of ctxt
+              yield_singleton (Variable.import_terms true) fully_skolemized_t ctxt
+              |>> Thm.cterm_of ctxt
           in
             (SOME (discharger_th, fully_skolemized_ct),
              (Thm.assume fully_skolemized_ct, ctxt))
diff -r 9bf04a8f211f -r aa7c49651f4e src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Jun 04 20:01:02 2019 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Jun 04 20:49:33 2019 +0200
@@ -1048,7 +1048,7 @@
 
 fun import_intros inp_pred [] ctxt =
       let
-        val ([outp_pred], ctxt') = Variable.import_terms true [inp_pred] ctxt
+        val (outp_pred, ctxt') = yield_singleton (Variable.import_terms true) inp_pred ctxt
         val T = fastype_of outp_pred
         val paramTs = ho_argsT_of_typ (binder_types T)
         val (param_names, _) = Variable.variant_fixes
diff -r 9bf04a8f211f -r aa7c49651f4e src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Tue Jun 04 20:01:02 2019 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Tue Jun 04 20:49:33 2019 +0200
@@ -466,7 +466,7 @@
 
 fun conv ctxt t =
   let
-    val ([t'], ctxt') = Variable.import_terms true [t] (Variable.declare_term t ctxt)
+    val (t', ctxt') = yield_singleton (Variable.import_terms true) t (Variable.declare_term t ctxt)
     val ct = Thm.cterm_of ctxt' t'
     fun unfold_conv thms =
       Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
diff -r 9bf04a8f211f -r aa7c49651f4e src/Provers/Arith/cancel_numeral_factor.ML
--- a/src/Provers/Arith/cancel_numeral_factor.ML	Tue Jun 04 20:01:02 2019 +0200
+++ b/src/Provers/Arith/cancel_numeral_factor.ML	Tue Jun 04 20:49:33 2019 +0200
@@ -45,7 +45,7 @@
   let
     val prems = Simplifier.prems_of ctxt;
     val t = Thm.term_of ct;
-    val ([t'], ctxt') = Variable.import_terms true [t] ctxt
+    val (t', ctxt') = yield_singleton (Variable.import_terms true) t ctxt
 
     val (t1,t2) = Data.dest_bal t'
     val (m1, t1') = Data.dest_coeff t1
diff -r 9bf04a8f211f -r aa7c49651f4e src/Provers/Arith/cancel_numerals.ML
--- a/src/Provers/Arith/cancel_numerals.ML	Tue Jun 04 20:01:02 2019 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML	Tue Jun 04 20:49:33 2019 +0200
@@ -69,7 +69,7 @@
   let
     val prems = Simplifier.prems_of ctxt
     val t = Thm.term_of ct
-    val ([t'], ctxt') = Variable.import_terms true [t] ctxt
+    val (t', ctxt') = yield_singleton (Variable.import_terms true) t ctxt
 
     val (t1,t2) = Data.dest_bal t'
     val terms1 = Data.dest_sum t1
diff -r 9bf04a8f211f -r aa7c49651f4e src/Provers/Arith/combine_numerals.ML
--- a/src/Provers/Arith/combine_numerals.ML	Tue Jun 04 20:01:02 2019 +0200
+++ b/src/Provers/Arith/combine_numerals.ML	Tue Jun 04 20:49:33 2019 +0200
@@ -68,7 +68,7 @@
 fun proc ctxt ct =
   let
     val t = Thm.term_of ct
-    val ([t'], ctxt') = Variable.import_terms true [t] ctxt
+    val (t', ctxt') = yield_singleton (Variable.import_terms true) t ctxt
 
     val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
     val T = Term.fastype_of u
diff -r 9bf04a8f211f -r aa7c49651f4e src/Provers/Arith/extract_common_term.ML
--- a/src/Provers/Arith/extract_common_term.ML	Tue Jun 04 20:01:02 2019 +0200
+++ b/src/Provers/Arith/extract_common_term.ML	Tue Jun 04 20:49:33 2019 +0200
@@ -49,7 +49,7 @@
 fun proc ctxt t =
   let
     val prems = Simplifier.prems_of ctxt;
-    val ([t'], ctxt') = Variable.import_terms true [t] ctxt
+    val (t', ctxt') = yield_singleton (Variable.import_terms true) t ctxt
 
     val (t1,t2) = Data.dest_bal t'
     val terms1 = Data.dest_sum t1
diff -r 9bf04a8f211f -r aa7c49651f4e src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Tue Jun 04 20:01:02 2019 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML	Tue Jun 04 20:49:33 2019 +0200
@@ -30,7 +30,7 @@
   let
     val t = Const (c, Consts.type_scheme (Proof_Context.consts_of ctxt) c)
       handle TYPE (msg, _, _) => error msg;
-    val ([t'], _) = Variable.import_terms true [t] ctxt;
+    val (t', _) = yield_singleton (Variable.import_terms true) t ctxt;
   in Thy_Output.pretty_term ctxt t' end;
 
 fun pretty_abbrev ctxt s =