# HG changeset patch
# User wenzelm
# Date 1565101768 -7200
# Node ID cf66d2db97fe7ea8f235c2d573f236b766608407
# Parent  1004333b76aaf7dd18527f19c973dd27a7a1c108
more robust and convenient treatment of implicit context;

diff -r 1004333b76aa -r cf66d2db97fe src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Aug 06 16:15:22 2019 +0200
+++ b/src/Pure/drule.ML	Tue Aug 06 16:29:28 2019 +0200
@@ -281,7 +281,8 @@
 (*Resolution: multiple arguments, multiple results*)
 local
   fun res opt_ctxt th i rule =
-    Thm.biresolution opt_ctxt false [(false, th)] i rule handle THM _ => Seq.empty;
+    (Thm.biresolution opt_ctxt false [(false, th)] i rule handle THM _ => Seq.empty)
+    |> Seq.map Thm.solve_constraints;
 
   fun multi_res _ _ [] rule = Seq.single rule
     | multi_res opt_ctxt i (th :: ths) rule =
@@ -297,14 +298,14 @@
   let
     val resolve = Thm.biresolution NONE false (map (pair false) thas) i
     fun resb thb = Seq.list_of (resolve thb) handle THM _ => []
-  in maps resb thbs end;
+  in maps resb thbs |> map Thm.solve_constraints end;
 
 fun thas RL thbs = thas RLN (1, thbs);
 
 (*Isar-style multi-resolution*)
 fun bottom_rl OF rls =
   (case Seq.chop 2 (multi_resolve NONE rls bottom_rl) of
-    ([th], _) => th
+    ([th], _) => Thm.solve_constraints th
   | ([], _) => raise THM ("OF: no unifiers", 0, bottom_rl :: rls)
   | _ => raise THM ("OF: multiple unifiers", 0, bottom_rl :: rls));
 
@@ -318,7 +319,8 @@
 fun compose (tha, i, thb) =
   Thm.bicompose NONE {flatten = true, match = false, incremented = false} (false, tha, 0) i thb
   |> Seq.list_of |> distinct Thm.eq_thm
-  |> (fn [th] => th | _ => raise THM ("compose: unique result expected", i, [tha, thb]));
+  |> (fn [th] => Thm.solve_constraints th
+       | _ => raise THM ("compose: unique result expected", i, [tha, thb]));
 
 
 (** theorem equality **)
@@ -695,7 +697,7 @@
   Thm.bicompose NONE {flatten = true, match = false, incremented = incremented}
     (false, th1, 0) 1 th2
   |> Seq.list_of |> distinct Thm.eq_thm
-  |> (fn [th] => th | _ => raise THM ("COMP", 1, [th1, th2]));
+  |> (fn [th] => Thm.solve_constraints th | _ => raise THM ("COMP", 1, [th1, th2]));
 
 in
 
@@ -709,7 +711,7 @@
   (case distinct Thm.eq_thm (Seq.list_of
       (Thm.bicompose NONE {flatten = false, match = false, incremented = true}
         (false, th, n) i (incr_indexes th rule))) of
-    [th'] => th'
+    [th'] => Thm.solve_constraints th'
   | [] => raise THM ("comp_no_flatten", i, [th, rule])
   | _ => raise THM ("comp_no_flatten: unique result expected", i, [th, rule]));
 
diff -r 1004333b76aa -r cf66d2db97fe src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Tue Aug 06 16:15:22 2019 +0200
+++ b/src/Pure/raw_simplifier.ML	Tue Aug 06 16:29:28 2019 +0200
@@ -533,7 +533,9 @@
       if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (Thm.term_of elhs)
       then mk_eq_True ctxt (thm, name)
       else rrule_eq_True ctxt thm name lhs elhs rhs thm
-  end;
+  end |> map (fn {thm, name, lhs, elhs, perm} =>
+    {thm = Thm.trim_context thm, name = name, lhs = lhs,
+      elhs = Thm.trim_context_cterm elhs, perm = perm});
 
 fun orient_rrule ctxt (thm, name) =
   let
@@ -690,8 +692,7 @@
         raise SIMPLIFIER ("Congruence must start with a constant", [thm]);
       val (xs, _) = congs;
       val xs' = filter_out (fn (x : cong_name, _) => x = a) xs;
-      val weak' = xs' |> map_filter (fn (a, thm) =>
-        if is_full_cong thm then NONE else SOME a);
+      val weak' = xs' |> map_filter (fn (a, th) => if is_full_cong th then NONE else SOME a);
     in ((xs', weak'), procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) end);
 
 fun add_cong thm ctxt = add_eqcong (mk_cong ctxt thm) ctxt;
@@ -1351,7 +1352,11 @@
     val _ =
       cond_tracing ctxt (fn () =>
         print_term ctxt "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" (Thm.term_of ct));
-  in bottomc (mode, Option.map (Drule.flexflex_unique (SOME ctxt)) oo prover, maxidx) ctxt ct end;
+  in
+    ct
+    |> bottomc (mode, Option.map (Drule.flexflex_unique (SOME ctxt)) oo prover, maxidx) ctxt
+    |> Thm.solve_constraints
+  end;
 
 val simple_prover =
   SINGLE o (fn ctxt => ALLGOALS (resolve_tac ctxt (prems_of ctxt)));
diff -r 1004333b76aa -r cf66d2db97fe src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Aug 06 16:15:22 2019 +0200
+++ b/src/Pure/thm.ML	Tue Aug 06 16:29:28 2019 +0200
@@ -1575,6 +1575,7 @@
           hyps = hyps,
           tpairs = tpairs',
           prop = prop'})
+        |> solve_constraints
       end
       handle TYPE (msg, _, _) => raise THM (msg, 0, [th]);
 
@@ -2154,7 +2155,7 @@
 (*Resolution: exactly one resolvent must be produced*)
 fun tha RSN (i, thb) =
   (case Seq.chop 2 (biresolution NONE false [(false, tha)] i thb) of
-    ([th], _) => th
+    ([th], _) => solve_constraints th
   | ([], _) => raise THM ("RSN: no unifiers", i, [tha, thb])
   | _ => raise THM ("RSN: multiple unifiers", i, [tha, thb]));