# HG changeset patch # User wenzelm # Date 1117533216 -7200 # Node ID 1bb17485602fee7e90d9db94eda70391a4d41ec1 # Parent e339119f4261b17ba264627f876391745912b7e4 renamed cond_extern to extern; Sign.declare_name replaces NameSpace.extend; (RAW_)METHOD_CASES: RuleCases.T option; diff -r e339119f4261 -r 1bb17485602f src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Tue May 31 11:53:35 2005 +0200 +++ b/src/Pure/Isar/method.ML Tue May 31 11:53:36 2005 +0200 @@ -19,10 +19,10 @@ val trace: Proof.context -> thm list -> unit val RAW_METHOD: (thm list -> tactic) -> Proof.method val RAW_METHOD_CASES: - (thm list -> thm -> (thm * (string * RuleCases.T) list) Seq.seq) -> Proof.method + (thm list -> thm -> (thm * (string * RuleCases.T option) list) Seq.seq) -> Proof.method val METHOD: (thm list -> tactic) -> Proof.method val METHOD_CASES: - (thm list -> thm -> (thm * (string * RuleCases.T) list) Seq.seq) -> Proof.method + (thm list -> thm -> (thm * (string * RuleCases.T option) list) Seq.seq) -> Proof.method val SIMPLE_METHOD: tactic -> Proof.method val SIMPLE_METHOD': ((int -> tactic) -> tactic) -> (int -> tactic) -> Proof.method val fail: Proof.method @@ -183,8 +183,8 @@ (* unfold/fold definitions *) -fun unfold ths = SIMPLE_METHOD (CHANGED_PROP (rewrite_goals_tac ths)); -fun fold ths = SIMPLE_METHOD (CHANGED_PROP (fold_goals_tac ths)); +fun unfold_meth ths = SIMPLE_METHOD (CHANGED_PROP (rewrite_goals_tac ths)); +fun fold_meth ths = SIMPLE_METHOD (CHANGED_PROP (fold_goals_tac ths)); (* atomize rule statements *) @@ -522,7 +522,7 @@ fun prt_meth (name, ((_, comment), _)) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; in - [Pretty.big_list "methods:" (map prt_meth (NameSpace.cond_extern_table space meths))] + [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table space meths))] |> Pretty.chunks |> Pretty.writeln end; end; @@ -556,17 +556,15 @@ fun add_methods raw_meths thy = let - val full = Sign.full_name (Theory.sign_of thy); - val new_meths = - map (fn (name, f, comment) => (full name, ((f, comment), stamp ()))) raw_meths; + val sg = Theory.sign_of thy; + val new_meths = raw_meths |> map (fn (name, f, comment) => + (Sign.full_name sg name, ((f, comment), stamp ()))); val {space, meths} = MethodsData.get thy; - val space' = NameSpace.extend (space, map fst new_meths); + val space' = fold (Sign.declare_name sg) (map fst new_meths) space; val meths' = Symtab.extend (meths, new_meths) handle Symtab.DUPS dups => error ("Duplicate declaration of method(s) " ^ commas_quote dups); - in - thy |> MethodsData.put {space = space', meths = meths'} - end; + in thy |> MethodsData.put {space = space', meths = meths'} end; val add_method = add_methods o Library.single; @@ -784,10 +782,10 @@ ("succeed", no_args succeed, "succeed"), ("-", no_args insert_facts, "do nothing (insert current facts only)"), ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"), - ("unfold", thms_args unfold, "unfold definitions"), + ("unfold", thms_args unfold_meth, "unfold definitions"), ("intro", thms_args intro, "repeatedly apply introduction rules"), ("elim", thms_args elim, "repeatedly apply elimination rules"), - ("fold", thms_args fold, "fold definitions"), + ("fold", thms_args fold_meth, "fold definitions"), ("atomize", (atomize o #2) oo syntax (Args.mode "full"), "present local premises as object-level statements"), ("rules", rules_args rules_meth, "apply many rules, including proof search"), @@ -812,6 +810,10 @@ val _ = Context.add_setup [add_methods pure_methods]; +(*final declarations of this structure!*) +val unfold = unfold_meth; +val fold = fold_meth; + end; structure BasicMethod: BASIC_METHOD = Method;