# HG changeset patch # User wenzelm # Date 1191942680 -7200 # Node ID 68a36883f0ad1ead64a3c820153762146c2023d4 # Parent a033971c63a0f12dcc2c186a13699b2e73727299 TheoryTarget.init_cmd; diff -r a033971c63a0 -r 68a36883f0ad src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Tue Oct 09 17:10:49 2007 +0200 +++ b/src/Pure/Isar/toplevel.ML Tue Oct 09 17:11:20 2007 +0200 @@ -114,7 +114,7 @@ type generic_theory = Context.generic; (*theory or local_theory*) -val loc_init = TheoryTarget.init; +val loc_init = TheoryTarget.init_cmd; val loc_exit = ProofContext.theory_of o LocalTheory.exit;