src/Tools/induct.ML
changeset 51580 64ef8260dc60
parent 49748 a346daa8a1f4
child 51584 98029ceda8ce
     1.1 --- a/src/Tools/induct.ML	Fri Mar 29 22:13:02 2013 +0100
     1.2 +++ b/src/Tools/induct.ML	Fri Mar 29 22:14:27 2013 +0100
     1.3 @@ -213,7 +213,7 @@
     1.4  
     1.5  fun pretty_rules ctxt kind rs =
     1.6    let val thms = map snd (Item_Net.content rs)
     1.7 -  in Pretty.big_list kind (map (Display.pretty_thm ctxt) thms) end;
     1.8 +  in Pretty.big_list kind (map (Pretty.item o single o Display.pretty_thm ctxt) thms) end;
     1.9  
    1.10  
    1.11  (* context data *)