# HG changeset patch
# User wenzelm
# Date 1154000643 -7200
# Node ID 54e15870444bca950b4068a405a79119732407bb
# Parent  3cbf73ed92f87c1b2159929639560de6eef8822a
"moved basic assumption operations from structure ProofContext to Assumption;"

diff -r 3cbf73ed92f8 -r 54e15870444b src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Thu Jul 27 13:43:13 2006 +0200
+++ b/src/Pure/Isar/local_theory.ML	Thu Jul 27 13:44:03 2006 +0200
@@ -137,7 +137,7 @@
       |> (fn (params, ctxt) => Data.put
           {locale = SOME (loc, ctxt),
            params = params,
-           hyps = ProofContext.assms_of ctxt,
+           hyps = Assumption.assms_of ctxt,
            restore_naming = Sign.restore_naming thy} ctxt);
 
 fun init loc thy = init_i (Option.map (Locale.intern thy) loc) thy;