src/Pure/raw_simplifier.ML
changeset 57859 29e728588163
parent 56438 7f6b2634d853
child 58836 4037bb00d08e
     1.1 --- a/src/Pure/raw_simplifier.ML	Tue Aug 05 11:06:36 2014 +0200
     1.2 +++ b/src/Pure/raw_simplifier.ML	Tue Aug 05 12:01:32 2014 +0200
     1.3 @@ -385,7 +385,7 @@
     1.4      val thy' = Proof_Context.theory_of ctxt';
     1.5    in Context.theory_map (Simpset.map (K (simpset_of ctxt'))) thy' end;
     1.6  
     1.7 -fun map_ss f = Context.mapping (map_theory_simpset f) f;
     1.8 +fun map_ss f = Context.mapping (map_theory_simpset (f o Context_Position.not_really)) f;
     1.9  
    1.10  val clear_simpset =
    1.11    map_simpset (fn Simpset ({depth, ...}, {mk_rews, termless, subgoal_tac, solvers, ...}) =>
    1.12 @@ -428,7 +428,7 @@
    1.13  val simp_trace = Config.bool simp_trace_raw;
    1.14  
    1.15  fun cond_warning ctxt msg =
    1.16 -  if Context_Position.is_visible ctxt then warning (msg ()) else ();
    1.17 +  if Context_Position.is_really_visible ctxt then warning (msg ()) else ();
    1.18  
    1.19  fun cond_tracing' ctxt flag msg =
    1.20    if Config.get ctxt flag then
    1.21 @@ -593,6 +593,7 @@
    1.22  fun add_simp thm ctxt = ctxt addsimps [thm];
    1.23  fun del_simp thm ctxt = ctxt delsimps [thm];
    1.24  
    1.25 +
    1.26  (* congs *)
    1.27  
    1.28  local