src/Tools/induct.ML
changeset 32111 30e2ffbba718
parent 32043 a6a6e8031c14
child 32171 220abde9962b
     1.1 --- a/src/Tools/induct.ML	Tue Jul 21 00:56:19 2009 +0200
     1.2 +++ b/src/Tools/induct.ML	Tue Jul 21 01:03:18 2009 +0200
     1.3 @@ -124,7 +124,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 (ProofContext.pretty_thm ctxt) thms) end;
     1.8 +  in Pretty.big_list kind (map (Display.pretty_thm ctxt) thms) end;
     1.9  
    1.10  
    1.11  (* context data *)