Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Quotient/quotient_info.ML
changeset 59582 0fbed69ff081
parent 59157 949829bae42a
child 59936 b8ffc3dc9e24 
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Wed Mar 04 19:53:18 2015 +0100
@@ -125,7 +125,7 @@
           Pretty.str "relation map:",
           Pretty.str relmap,
           Pretty.str "quot. theorem:",
-          Syntax.pretty_term ctxt (prop_of quot_thm)])
+          Syntax.pretty_term ctxt (Thm.prop_of quot_thm)])
   in
     map prt_map (Symtab.dest (get_quotmaps (Context.Proof ctxt)))
     |> Pretty.big_list "maps for type constructors:"
@@ -178,9 +178,9 @@
         Pretty.str "relation:",
         Syntax.pretty_term ctxt equiv_rel,
         Pretty.str "equiv. thm:",
-        Syntax.pretty_term ctxt (prop_of equiv_thm),
+        Syntax.pretty_term ctxt (Thm.prop_of equiv_thm),
         Pretty.str "quot. thm:",
-        Syntax.pretty_term ctxt (prop_of quot_thm)])
+        Syntax.pretty_term ctxt (Thm.prop_of quot_thm)])
   in
     map (prt_quot o snd) (Symtab.dest (get_quotients (Context.Proof ctxt)))
     |> Pretty.big_list "quotients:"
@@ -218,7 +218,7 @@
         Pretty.str ":=",
         Syntax.pretty_term ctxt rconst,
         Pretty.str "as",
-        Syntax.pretty_term ctxt (prop_of def)])
+        Syntax.pretty_term ctxt (Thm.prop_of def)])
   in
     map prt_qconst (maps snd (Symtab.dest (get_quotconsts (Context.Proof ctxt))))
     |> Pretty.big_list "quotient constants:"
isabelle