src/FOLP/classical.ML
changeset 61268 abe08fb15a12
parent 60754 02924903a6fd
     1.1 --- a/src/FOLP/classical.ML	Fri Sep 25 20:04:25 2015 +0200
     1.2 +++ b/src/FOLP/classical.ML	Fri Sep 25 20:37:59 2015 +0200
     1.3 @@ -124,10 +124,10 @@
     1.4  
     1.5  fun print_cs ctxt (CS{safeIs,safeEs,hazIs,hazEs,...}) =
     1.6    writeln (cat_lines
     1.7 -   (["Introduction rules"] @ map (Display.string_of_thm ctxt) hazIs @
     1.8 -    ["Safe introduction rules"] @ map (Display.string_of_thm ctxt) safeIs @
     1.9 -    ["Elimination rules"] @ map (Display.string_of_thm ctxt) hazEs @
    1.10 -    ["Safe elimination rules"] @ map (Display.string_of_thm ctxt) safeEs));
    1.11 +   (["Introduction rules"] @ map (Thm.string_of_thm ctxt) hazIs @
    1.12 +    ["Safe introduction rules"] @ map (Thm.string_of_thm ctxt) safeIs @
    1.13 +    ["Elimination rules"] @ map (Thm.string_of_thm ctxt) hazEs @
    1.14 +    ["Safe elimination rules"] @ map (Thm.string_of_thm ctxt) safeEs));
    1.15  
    1.16  fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths =
    1.17    make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs};