src/ZF/Datatype_ZF.thy
changeset 26928 ca87aff1ad2d
parent 26480 544cef16045b
child 26939 1035c89b4c02
     1.1 --- a/src/ZF/Datatype_ZF.thy	Fri May 16 23:25:37 2008 +0200
     1.2 +++ b/src/ZF/Datatype_ZF.thy	Sat May 17 13:54:30 2008 +0200
     1.3 @@ -72,7 +72,7 @@
     1.4  
     1.5   fun proc sg ss old =
     1.6     let val _ = if !trace then writeln ("data_free: OLD = " ^ 
     1.7 -                                       string_of_cterm (cterm_of sg old))
     1.8 +                                       Display.string_of_cterm (cterm_of sg old))
     1.9                 else ()
    1.10         val (lhs,rhs) = FOLogic.dest_eq old
    1.11         val (lhead, largs) = strip_comb lhs
    1.12 @@ -90,7 +90,7 @@
    1.13                 else Const("False",FOLogic.oT)
    1.14             else raise Match
    1.15         val _ = if !trace then 
    1.16 -                 writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new))
    1.17 +                 writeln ("NEW = " ^ Display.string_of_cterm (Thm.cterm_of sg new))
    1.18                 else ();
    1.19         val goal = Logic.mk_equals (old, new)
    1.20         val thm = Goal.prove (Simplifier.the_context ss) [] [] goal