# HG changeset patch
# User ballarin
# Date 1280613485 -7200
# Node ID 77f56abf158bb887ecdd2e9ed84d3b8075a00f57
# Parent  2c1913d1b945713b1c3d04bc10b3e1fd4ef123b9
More consistent naming of locale api functions.

diff -r 2c1913d1b945 -r 77f56abf158b src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Jul 31 23:32:05 2010 +0200
+++ b/src/Pure/Isar/locale.ML	Sat Jul 31 23:58:05 2010 +0200
@@ -70,7 +70,7 @@
     morphism -> Context.generic -> Context.generic
   val amend_registration: string * morphism -> morphism * bool ->
     morphism -> Context.generic -> Context.generic
-  val registrations_of_locale: Context.generic -> string -> (string * morphism) list
+  val registrations_of: Context.generic -> string -> (string * morphism) list
   val add_dependency: string -> string * morphism -> morphism -> theory -> theory
 
   (* Diagnostic *)
@@ -421,7 +421,7 @@
   |-> (fn regs => fn _ => map (fn ((name, _), ((base, export) ,_)) =>
     (name, base $> (collect_mixins context (name, base $> export)) $> export)) regs);
 
-fun registrations_of_locale context name =
+fun registrations_of context name =
   get_registrations context (filter (curry (op =) name o fst o fst));
 
 fun all_registrations context = get_registrations context I;
@@ -518,7 +518,7 @@
               val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
                 Attrib.map_facts (Attrib.attribute_i thy)
             in PureThy.note_thmss kind args'' #> snd end)
-        (registrations_of_locale (Context.Theory thy) loc) thy))
+        (registrations_of (Context.Theory thy) loc) thy))
   in ctxt'' end;
 
 
@@ -604,7 +604,7 @@
   let
     val thy = ProofContext.theory_of ctxt;
   in
-    (case registrations_of_locale  (Context.Proof ctxt) (* FIXME *) (intern thy raw_name) of
+    (case registrations_of  (Context.Proof ctxt) (* FIXME *) (intern thy raw_name) of
         [] => Pretty.str ("no interpretations")
       | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
     |> Pretty.writeln
@@ -618,7 +618,7 @@
         val params = params_of thy name;
         val axioms = (these o Option.map (Logic.strip_imp_prems o Thm.prop_of) o fst o intros_of thy) name;
         val registrations = map (instance_of thy name o snd)
-          (registrations_of_locale (Context.Theory thy) name);
+          (registrations_of (Context.Theory thy) name);
       in 
         Graph.new_node (name, { params = params, axioms = axioms, registrations = registrations })
       end;
diff -r 2c1913d1b945 -r 77f56abf158b src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Sat Jul 31 23:32:05 2010 +0200
+++ b/src/Tools/quickcheck.ML	Sat Jul 31 23:58:05 2010 +0200
@@ -228,7 +228,7 @@
     val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi));
     val check_goals = case some_locale
      of NONE => [proto_goal]
-      | SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal) (Locale.registrations_of_locale (Context.Theory thy) (*FIXME*) locale);
+      | SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal) (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
     val inst_goals = maps (fn check_goal => map (fn T =>
       Term ((Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
         handle WELLSORTED s => Wellsorted_Error s) default_Ts) check_goals