src/FOLP/classical.ML
changeset 42439 9efdd0af15ac
parent 37744 3daaf23b9ab4
child 42799 4e33894aec6d
     1.1 --- a/src/FOLP/classical.ML	Wed Apr 20 17:17:01 2011 +0200
     1.2 +++ b/src/FOLP/classical.ML	Wed Apr 20 22:57:29 2011 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4    val addSDs: claset * thm list -> claset
     1.5    val addSEs: claset * thm list -> claset
     1.6    val addSIs: claset * thm list -> claset
     1.7 -  val print_cs: claset -> unit
     1.8 +  val print_cs: Proof.context -> claset -> unit
     1.9    val rep_cs: claset -> 
    1.10        {safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list, 
    1.11         safe0_brls:(bool*thm)list, safep_brls: (bool*thm)list,
    1.12 @@ -122,12 +122,12 @@
    1.13  
    1.14  val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]};
    1.15  
    1.16 -fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) =
    1.17 +fun print_cs ctxt (CS{safeIs,safeEs,hazIs,hazEs,...}) =
    1.18    writeln (cat_lines
    1.19 -   (["Introduction rules"] @ map Display.string_of_thm_without_context hazIs @
    1.20 -    ["Safe introduction rules"] @ map Display.string_of_thm_without_context safeIs @
    1.21 -    ["Elimination rules"] @ map Display.string_of_thm_without_context hazEs @
    1.22 -    ["Safe elimination rules"] @ map Display.string_of_thm_without_context safeEs));
    1.23 +   (["Introduction rules"] @ map (Display.string_of_thm ctxt) hazIs @
    1.24 +    ["Safe introduction rules"] @ map (Display.string_of_thm ctxt) safeIs @
    1.25 +    ["Elimination rules"] @ map (Display.string_of_thm ctxt) hazEs @
    1.26 +    ["Safe elimination rules"] @ map (Display.string_of_thm ctxt) safeEs));
    1.27  
    1.28  fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths =
    1.29    make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs};