| changeset 35205 | 611b90bb89bc |
| parent 33727 | e2d5d7f51aa3 |
| child 36315 | e859879079c8 |
--- a/src/Pure/Isar/toplevel.ML Thu Feb 18 23:38:33 2010 +0100 +++ b/src/Pure/Isar/toplevel.ML Thu Feb 18 23:41:01 2010 +0100 @@ -104,7 +104,7 @@ type generic_theory = Context.generic; (*theory or local_theory*) -val loc_init = Theory_Target.context; +val loc_init = Theory_Target.context_cmd; val loc_exit = Local_Theory.exit_global; fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy