# HG changeset patch # User wenzelm # Date 1144922468 -7200 # Node ID 177e35232d1b70792a9bef59112697bd4ab94fe1 # Parent e425e74b01aff20b2c68194b4ec48b4d450807e5 ProofDisplay.print_theorems/theory; diff -r e425e74b01af -r 177e35232d1b src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Thu Apr 13 12:01:07 2006 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Thu Apr 13 12:01:08 2006 +0200 @@ -219,7 +219,7 @@ val print_context = Toplevel.keep Toplevel.print_state_context; val print_theory = Toplevel.unknown_theory o - Toplevel.keep (PureThy.print_theory o Toplevel.theory_of); + Toplevel.keep (ProofDisplay.print_theory o Toplevel.theory_of); val print_syntax = Toplevel.unknown_theory o Toplevel.keep (Display.print_syntax o Toplevel.theory_of) o @@ -232,8 +232,8 @@ val print_theorems_theory = Toplevel.keep (fn state => Toplevel.theory_of state |> (case Option.map Toplevel.theory_node (History.previous (Toplevel.node_history_of state)) of - SOME (SOME prev_thy) => PureThy.print_theorems_diff prev_thy - | _ => PureThy.print_theorems)); + SOME (SOME prev_thy) => ProofDisplay.print_theorems_diff prev_thy + | _ => ProofDisplay.print_theorems)); val print_theorems = Toplevel.unknown_theory o print_theorems_theory o print_theorems_proof;