1.1 --- a/src/Pure/Isar/method.ML	Tue May 31 11:53:35 2005 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Tue May 31 11:53:36 2005 +0200
     1.3 @@ -19,10 +19,10 @@
     1.4    val trace: Proof.context -> thm list -> unit
     1.5    val RAW_METHOD: (thm list -> tactic) -> Proof.method
     1.6    val RAW_METHOD_CASES:
     1.7 -    (thm list -> thm -> (thm * (string * RuleCases.T) list) Seq.seq) -> Proof.method
     1.8 +    (thm list -> thm -> (thm * (string * RuleCases.T option) list) Seq.seq) -> Proof.method
     1.9    val METHOD: (thm list -> tactic) -> Proof.method
    1.10    val METHOD_CASES:
    1.11 -    (thm list -> thm -> (thm * (string * RuleCases.T) list) Seq.seq) -> Proof.method
    1.12 +    (thm list -> thm -> (thm * (string * RuleCases.T option) list) Seq.seq) -> Proof.method
    1.13    val SIMPLE_METHOD: tactic -> Proof.method
    1.14    val SIMPLE_METHOD': ((int -> tactic) -> tactic) -> (int -> tactic) -> Proof.method
    1.15    val fail: Proof.method
    1.16 @@ -183,8 +183,8 @@
    1.17  
    1.18  (* unfold/fold definitions *)
    1.19  
    1.20 -fun unfold ths = SIMPLE_METHOD (CHANGED_PROP (rewrite_goals_tac ths));
    1.21 -fun fold ths = SIMPLE_METHOD (CHANGED_PROP (fold_goals_tac ths));
    1.22 +fun unfold_meth ths = SIMPLE_METHOD (CHANGED_PROP (rewrite_goals_tac ths));
    1.23 +fun fold_meth ths = SIMPLE_METHOD (CHANGED_PROP (fold_goals_tac ths));
    1.24  
    1.25  
    1.26  (* atomize rule statements *)
    1.27 @@ -522,7 +522,7 @@
    1.28        fun prt_meth (name, ((_, comment), _)) = Pretty.block
    1.29          [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    1.30      in
    1.31 -      [Pretty.big_list "methods:" (map prt_meth (NameSpace.cond_extern_table space meths))]
    1.32 +      [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table space meths))]
    1.33        |> Pretty.chunks |> Pretty.writeln
    1.34      end;
    1.35  end;
    1.36 @@ -556,17 +556,15 @@
    1.37  
    1.38  fun add_methods raw_meths thy =
    1.39    let
    1.40 -    val full = Sign.full_name (Theory.sign_of thy);
    1.41 -    val new_meths =
    1.42 -      map (fn (name, f, comment) => (full name, ((f, comment), stamp ()))) raw_meths;
    1.43 +    val sg = Theory.sign_of thy;
    1.44 +    val new_meths = raw_meths |> map (fn (name, f, comment) =>
    1.45 +      (Sign.full_name sg name, ((f, comment), stamp ())));
    1.46  
    1.47      val {space, meths} = MethodsData.get thy;
    1.48 -    val space' = NameSpace.extend (space, map fst new_meths);
    1.49 +    val space' = fold (Sign.declare_name sg) (map fst new_meths) space;
    1.50      val meths' = Symtab.extend (meths, new_meths) handle Symtab.DUPS dups =>
    1.51        error ("Duplicate declaration of method(s) " ^ commas_quote dups);
    1.52 -  in
    1.53 -    thy |> MethodsData.put {space = space', meths = meths'}
    1.54 -  end;
    1.55 +  in thy |> MethodsData.put {space = space', meths = meths'} end;
    1.56  
    1.57  val add_method = add_methods o Library.single;
    1.58  
    1.59 @@ -784,10 +782,10 @@
    1.60    ("succeed", no_args succeed, "succeed"),
    1.61    ("-", no_args insert_facts, "do nothing (insert current facts only)"),
    1.62    ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"),
    1.63 -  ("unfold", thms_args unfold, "unfold definitions"),
    1.64 +  ("unfold", thms_args unfold_meth, "unfold definitions"),
    1.65    ("intro", thms_args intro, "repeatedly apply introduction rules"),
    1.66    ("elim", thms_args elim, "repeatedly apply elimination rules"),
    1.67 -  ("fold", thms_args fold, "fold definitions"),
    1.68 +  ("fold", thms_args fold_meth, "fold definitions"),
    1.69    ("atomize", (atomize o #2) oo syntax (Args.mode "full"),
    1.70      "present local premises as object-level statements"),
    1.71    ("rules", rules_args rules_meth, "apply many rules, including proof search"),
    1.72 @@ -812,6 +810,10 @@
    1.73  val _ = Context.add_setup [add_methods pure_methods];
    1.74  
    1.75  
    1.76 +(*final declarations of this structure!*)
    1.77 +val unfold = unfold_meth;
    1.78 +val fold = fold_meth;
    1.79 +
    1.80  end;
    1.81  
    1.82  structure BasicMethod: BASIC_METHOD = Method;