--- 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 *)
--- 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');
--- 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;
--- 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;
--- 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) =
--- 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)
--- 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))
--- 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
--- 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))
--- 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
--- 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
--- 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
--- 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
--- 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 =