# HG changeset patch
# User wenzelm
# Date 1394460241 -3600
# Node ID 893fe12639bc76381db98692f41c5d8bf0f926da
# Parent  d74fed45fa8b31eb5c63999282be392039677334
tuned signature -- prefer Name_Space.get with its builtin error;

diff -r d74fed45fa8b -r 893fe12639bc src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Mar 10 13:55:03 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Mar 10 15:04:01 2014 +0100
@@ -954,8 +954,7 @@
 
 fun pointer_of_bundle_name bundle_name ctxt =
   let
-    val bundle_name = Bundle.check ctxt bundle_name
-    val bundle = Bundle.the_bundle ctxt bundle_name
+    val bundle = Bundle.get_bundle_cmd ctxt bundle_name
   in
     case bundle of
       [(_, [arg_src])] => 
diff -r d74fed45fa8b -r 893fe12639bc src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Mar 10 13:55:03 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Mon Mar 10 15:04:01 2014 +0100
@@ -142,11 +142,10 @@
 fun attribute_generic context =
   let val table = get_attributes context in
     fn src =>
-      let val ((name, _), pos) = Args.dest_src src in
-        (case Name_Space.lookup_key table name of
-          NONE => error ("Undefined attribute: " ^ quote name ^ Position.here pos)
-        | SOME (_, (att, _)) => att src)
-      end
+      let
+        val ((name, _), _) = Args.dest_src src;
+        val (att, _) = Name_Space.get table name;
+      in att src end
   end;
 
 val attribute = attribute_generic o Context.Proof;
diff -r d74fed45fa8b -r 893fe12639bc src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Mon Mar 10 13:55:03 2014 +0100
+++ b/src/Pure/Isar/bundle.ML	Mon Mar 10 15:04:01 2014 +0100
@@ -7,8 +7,9 @@
 signature BUNDLE =
 sig
   type bundle = (thm list * Args.src list) list
-  val the_bundle: Proof.context -> string -> bundle
   val check: Proof.context -> xstring * Position.T -> string
+  val get_bundle: Proof.context -> string -> bundle
+  val get_bundle_cmd: Proof.context -> xstring * Position.T -> bundle
   val bundle: binding * (thm list * Args.src list) list ->
     (binding * typ option * mixfix) list -> local_theory -> local_theory
   val bundle_cmd: binding * (Facts.ref * Args.src list) list ->
@@ -45,12 +46,10 @@
 
 val get_bundles = Data.get o Context.Proof;
 
-fun the_bundle ctxt name =
-  (case Name_Space.lookup_key (get_bundles ctxt) name of
-    SOME (_, bundle) => bundle
-  | NONE => error ("Unknown bundle " ^ quote name));
+fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt);
 
-fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt);
+val get_bundle = Name_Space.get o get_bundles;
+fun get_bundle_cmd ctxt = get_bundle ctxt o check ctxt;
 
 
 (* define bundle *)
@@ -85,17 +84,17 @@
 
 local
 
-fun gen_includes prep args ctxt =
-  let val decls = maps (the_bundle ctxt o prep ctxt) args
+fun gen_includes get args ctxt =
+  let val decls = maps (get ctxt) args
   in #2 (Attrib.local_notes "" [((Binding.empty, []), decls)] ctxt) end;
 
-fun gen_context prep_bundle prep_decl raw_incls raw_elems gthy =
+fun gen_context get prep_decl raw_incls raw_elems gthy =
   let
     val (after_close, lthy) =
       gthy |> Context.cases (pair Local_Theory.exit o Named_Target.theory_init)
         (pair I o Local_Theory.assert);
     val ((_, _, _, lthy'), _) = lthy
-      |> gen_includes prep_bundle raw_incls
+      |> gen_includes get raw_incls
       |> prep_decl ([], []) I raw_elems;
   in
     lthy' |> Local_Theory.open_target
@@ -104,8 +103,8 @@
 
 in
 
-val includes = gen_includes (K I);
-val includes_cmd = gen_includes check;
+val includes = gen_includes get_bundle;
+val includes_cmd = gen_includes get_bundle_cmd;
 
 fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.reset_facts;
 fun include_cmd bs =
@@ -114,8 +113,8 @@
 fun including bs = Proof.assert_backward #> Proof.map_context (includes bs);
 fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs);
 
-val context = gen_context (K I) Expression.cert_declaration;
-val context_cmd = gen_context check Expression.read_declaration;
+val context = gen_context get_bundle Expression.cert_declaration;
+val context_cmd = gen_context get_bundle_cmd Expression.read_declaration;
 
 end;
 
diff -r d74fed45fa8b -r 893fe12639bc src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon Mar 10 13:55:03 2014 +0100
+++ b/src/Pure/Isar/method.ML	Mon Mar 10 15:04:01 2014 +0100
@@ -353,11 +353,10 @@
 fun method ctxt =
   let val table = get_methods ctxt in
     fn src =>
-      let val ((name, _), pos) = Args.dest_src src in
-        (case Name_Space.lookup_key table name of
-          NONE => error ("Undefined method: " ^ quote name ^ Position.here pos)
-        | SOME (_, (meth, _)) => meth src)
-      end
+      let
+        val ((name, _), _) = Args.dest_src src;
+        val (meth, _) = Name_Space.get table name;
+      in meth src end
   end;
 
 fun method_cmd ctxt = method ctxt o check_src ctxt;
diff -r d74fed45fa8b -r 893fe12639bc src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Mon Mar 10 13:55:03 2014 +0100
+++ b/src/Pure/Isar/specification.ML	Mon Mar 10 15:04:01 2014 +0100
@@ -376,14 +376,14 @@
   fun merge data : T = Library.merge (eq_snd op =) data;
 );
 
-fun gen_theorem schematic prep_bundle prep_att prep_stmt
+fun gen_theorem schematic bundle_includes prep_att prep_stmt
     kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy =
   let
     val _ = Local_Theory.assert lthy;
 
     val elems = raw_elems |> map (Element.map_ctxt_attrib (prep_att lthy));
     val ((more_atts, prems, stmt, facts), goal_ctxt) = lthy
-      |> Bundle.includes (map (prep_bundle lthy) raw_includes)
+      |> bundle_includes raw_includes
       |> prep_statement (prep_att lthy) prep_stmt elems raw_concl;
     val atts = more_atts @ map (prep_att lthy) raw_atts;
 
@@ -419,13 +419,15 @@
 
 in
 
-val theorem = gen_theorem false (K I) (K I) Expression.cert_statement;
+val theorem =
+  gen_theorem false Bundle.includes (K I) Expression.cert_statement;
 val theorem_cmd =
-  gen_theorem false Bundle.check Attrib.check_src Expression.read_statement;
+  gen_theorem false Bundle.includes_cmd Attrib.check_src Expression.read_statement;
 
-val schematic_theorem = gen_theorem true (K I) (K I) Expression.cert_statement;
+val schematic_theorem =
+  gen_theorem true Bundle.includes (K I) Expression.cert_statement;
 val schematic_theorem_cmd =
-  gen_theorem true Bundle.check Attrib.check_src Expression.read_statement;
+  gen_theorem true Bundle.includes_cmd Attrib.check_src Expression.read_statement;
 
 fun add_theorem_hook f = Theorem_Hook.map (cons (f, stamp ()));
 
diff -r d74fed45fa8b -r 893fe12639bc src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Mar 10 13:55:03 2014 +0100
+++ b/src/Pure/sign.ML	Mon Mar 10 15:04:01 2014 +0100
@@ -192,7 +192,7 @@
 
 fun mk_const thy (c, Ts) = Const (c, const_instance thy (c, Ts));
 
-val declared_tyname = is_some oo (Name_Space.lookup_key o #types o Type.rep_tsig o tsig_of);
+fun declared_tyname ctxt c = can (Type.the_decl (tsig_of ctxt)) (c, Position.none);
 val declared_const = can o the_const_constraint;