src/HOL/Tools/inductive.ML
changeset 42439 9efdd0af15ac
parent 42381 309ec68442c6
child 42491 4bb5de0aae66
     1.1 --- a/src/HOL/Tools/inductive.ML	Wed Apr 20 17:17:01 2011 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Wed Apr 20 22:57:29 2011 +0200
     1.3 @@ -174,7 +174,7 @@
     1.4  val get_monos = #2 o get_inductives;
     1.5  val map_monos = InductiveData.map o apsnd;
     1.6  
     1.7 -fun mk_mono thm =
     1.8 +fun mk_mono ctxt thm =
     1.9    let
    1.10      fun eq2mono thm' = thm' RS (thm' RS eq_to_mono);
    1.11      fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD})
    1.12 @@ -187,11 +187,15 @@
    1.13        dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
    1.14          (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
    1.15      | _ => thm
    1.16 -  end handle THM _ =>
    1.17 -    error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm_without_context thm);
    1.18 +  end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm ctxt thm);
    1.19  
    1.20 -val mono_add = Thm.declaration_attribute (map_monos o Thm.add_thm o mk_mono);
    1.21 -val mono_del = Thm.declaration_attribute (map_monos o Thm.del_thm o mk_mono);
    1.22 +val mono_add =
    1.23 +  Thm.declaration_attribute (fn thm => fn context =>
    1.24 +    map_monos (Thm.add_thm (mk_mono (Context.proof_of context) thm)) context);
    1.25 +
    1.26 +val mono_del =
    1.27 +  Thm.declaration_attribute (fn thm => fn context =>
    1.28 +    map_monos (Thm.del_thm (mk_mono (Context.proof_of context) thm)) context);
    1.29  
    1.30  
    1.31  
    1.32 @@ -350,7 +354,7 @@
    1.33        REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1),
    1.34        REPEAT (FIRST
    1.35          [atac 1,
    1.36 -         resolve_tac (map mk_mono monos @ get_monos ctxt) 1,
    1.37 +         resolve_tac (map (mk_mono ctxt) monos @ get_monos ctxt) 1,
    1.38           etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])]));
    1.39  
    1.40