--- a/src/Pure/raw_simplifier.ML Tue Aug 05 11:06:36 2014 +0200
+++ b/src/Pure/raw_simplifier.ML Tue Aug 05 12:01:32 2014 +0200
@@ -385,7 +385,7 @@
val thy' = Proof_Context.theory_of ctxt';
in Context.theory_map (Simpset.map (K (simpset_of ctxt'))) thy' end;
-fun map_ss f = Context.mapping (map_theory_simpset f) f;
+fun map_ss f = Context.mapping (map_theory_simpset (f o Context_Position.not_really)) f;
val clear_simpset =
map_simpset (fn Simpset ({depth, ...}, {mk_rews, termless, subgoal_tac, solvers, ...}) =>
@@ -428,7 +428,7 @@
val simp_trace = Config.bool simp_trace_raw;
fun cond_warning ctxt msg =
- if Context_Position.is_visible ctxt then warning (msg ()) else ();
+ if Context_Position.is_really_visible ctxt then warning (msg ()) else ();
fun cond_tracing' ctxt flag msg =
if Config.get ctxt flag then
@@ -593,6 +593,7 @@
fun add_simp thm ctxt = ctxt addsimps [thm];
fun del_simp thm ctxt = ctxt delsimps [thm];
+
(* congs *)
local