# HG changeset patch # User wenzelm # Date 1154000581 -7200 # Node ID 9c40a144ee0e133fbf62f1bfe0ece71cd61786fc # Parent 89d2758ecddf6dc041bcb4fea7a9241bd0e70656 moved basic assumption operations from structure ProofContext to Assumption; diff -r 89d2758ecddf -r 9c40a144ee0e src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Thu Jul 27 13:43:00 2006 +0200 +++ b/src/HOL/Import/shuffler.ML Thu Jul 27 13:43:01 2006 +0200 @@ -665,7 +665,7 @@ fun search_meth ctxt = let val thy = ProofContext.theory_of ctxt - val prems = ProofContext.prems_of ctxt + val prems = Assumption.prems_of ctxt in Method.SIMPLE_METHOD' HEADGOAL (gen_shuffle_tac thy true (map (pair "premise") prems)) end diff -r 89d2758ecddf -r 9c40a144ee0e src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Thu Jul 27 13:43:00 2006 +0200 +++ b/src/HOL/Tools/res_atp.ML Thu Jul 27 13:43:01 2006 +0200 @@ -576,7 +576,7 @@ fun cnf_hyps_thms ctxt = - let val ths = ProofContext.prems_of ctxt + let val ths = Assumption.prems_of ctxt in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end; diff -r 89d2758ecddf -r 9c40a144ee0e src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Thu Jul 27 13:43:00 2006 +0200 +++ b/src/Pure/Isar/args.ML Thu Jul 27 13:43:01 2006 +0200 @@ -320,7 +320,7 @@ nat >> PureThy.Single)); val bang_facts = Scan.peek (fn context => - $$$ "!" >> K (ProofContext.prems_of (Context.proof_of context)) || Scan.succeed []); + $$$ "!" >> K (Assumption.prems_of (Context.proof_of context)) || Scan.succeed []); (* goal specification *) diff -r 89d2758ecddf -r 9c40a144ee0e src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Thu Jul 27 13:43:00 2006 +0200 +++ b/src/Pure/Isar/local_defs.ML Thu Jul 27 13:43:01 2006 +0200 @@ -10,7 +10,7 @@ val cert_def: ProofContext.context -> term -> (string * typ) * term val abs_def: term -> (string * typ) * term val mk_def: ProofContext.context -> (string * term) list -> term list - val def_export: ProofContext.export + val def_export: Assumption.export val add_def: string * term -> ProofContext.context -> ((string * typ) * thm) * ProofContext.context val print_rules: Context.generic -> unit diff -r 89d2758ecddf -r 9c40a144ee0e src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Jul 27 13:43:00 2006 +0200 +++ b/src/Pure/Isar/locale.ML Thu Jul 27 13:43:01 2006 +0200 @@ -1816,7 +1816,8 @@ val pred_ctxt = ProofContext.init pred_thy; val (ctxt, (_, facts)) = activate_facts true (K I) (pred_ctxt, axiomify predicate_axioms elemss'); - val export = ProofContext.export_view predicate_statement ctxt thy_ctxt; + val export = singleton (ProofContext.export_standard + (Assumption.add_view thy_ctxt predicate_statement ctxt) thy_ctxt); val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])])); val elems' = maps #2 (filter (equal "" o #1 o #1) elemss'); val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems'; diff -r 89d2758ecddf -r 9c40a144ee0e src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Thu Jul 27 13:43:00 2006 +0200 +++ b/src/Pure/Isar/method.ML Thu Jul 27 13:43:01 2006 +0200 @@ -227,7 +227,7 @@ fun assm_tac ctxt = assume_tac APPEND' - asm_tac (ProofContext.prems_of ctxt) APPEND' + asm_tac (Assumption.prems_of ctxt) APPEND' cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND' cond_rtac (can Logic.dest_term) Drule.termI; diff -r 89d2758ecddf -r 9c40a144ee0e src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Thu Jul 27 13:43:00 2006 +0200 +++ b/src/Pure/Isar/obtain.ML Thu Jul 27 13:43:01 2006 +0200 @@ -319,7 +319,7 @@ val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis)); in ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs)); - ctxt' |> ProofContext.add_assms_i ProofContext.assume_export + ctxt' |> ProofContext.add_assms_i Assumption.assume_export [((name, [ContextRules.intro_query NONE]), [(asm, [])])] |>> (fn [(_, [th])] => th) end; diff -r 89d2758ecddf -r 9c40a144ee0e src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Thu Jul 27 13:43:00 2006 +0200 +++ b/src/Pure/Isar/proof.ML Thu Jul 27 13:43:01 2006 +0200 @@ -47,9 +47,9 @@ val let_bind_i: (term list * term) list -> state -> state val fix: (string * string option * mixfix) list -> state -> state val fix_i: (string * typ option * mixfix) list -> state -> state - val assm: ProofContext.export -> + val assm: Assumption.export -> ((string * Attrib.src list) * (string * string list) list) list -> state -> state - val assm_i: ProofContext.export -> + val assm_i: Assumption.export -> ((string * attribute list) * (term * term list) list) list -> state -> state val assume: ((string * Attrib.src list) * (string * string list) list) list -> state -> state val assume_i: ((string * attribute list) * (term * term list) list) list -> state -> state @@ -476,10 +476,10 @@ val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks (pretty_goals_local ctxt "" (true, ! show_main_goal) (! Display.goals_limit) goal @ [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")]))); - val _ = - (case subtract (op aconv) (ProofContext.assms_of ctxt) (#hyps (Thm.rep_thm goal)) of - [] => () - | hyps => error ("Additional hypotheses:\n" ^ cat_lines (map string_of_term hyps))); + + val extra_hyps = Assumption.extra_hyps ctxt goal; + val _ = null extra_hyps orelse + error ("Additional hypotheses:\n" ^ cat_lines (map string_of_term extra_hyps)); val (results, th) = `(Conjunction.elim_precise (map length propss)) (Goal.conclude goal) handle THM _ => error ("Lost goal structure:\n" ^ string_of_thm goal); @@ -544,10 +544,10 @@ val assm = gen_assume ProofContext.add_assms Attrib.attribute; val assm_i = gen_assume ProofContext.add_assms_i (K I); -val assume = assm ProofContext.assume_export; -val assume_i = assm_i ProofContext.assume_export; -val presume = assm ProofContext.presume_export; -val presume_i = assm_i ProofContext.presume_export; +val assume = assm Assumption.assume_export; +val assume_i = assm_i Assumption.assume_export; +val presume = assm Assumption.presume_export; +val presume_i = assm_i Assumption.presume_export; end;