| changeset 32089 | 568a23753e3a |
| parent 32062 | 457f5bcd3d76 |
| child 32091 | 30e2ffbba718 |
--- a/src/Pure/Isar/proof.ML Mon Jul 20 20:03:19 2009 +0200 +++ b/src/Pure/Isar/proof.ML Mon Jul 20 21:20:09 2009 +0200 @@ -318,7 +318,7 @@ val show_main_goal = ref false; val verbose = ProofContext.verbose; -val pretty_goals_local = Display.pretty_goals_aux o Syntax.pp; +val pretty_goals_local = Display_Goal.pretty_goals_aux o Syntax.pp; fun pretty_facts _ _ NONE = [] | pretty_facts s ctxt (SOME ths) =