# HG changeset patch
# User ballarin
# Date 1142536765 -3600
# Node ID ac90764bb654819dd2fd84e67c2a984d80b6029d
# Parent  3d10de7a8ca7aa6baa5b0a449c89fcc6d969ac4e
New interface function parameters_of_expr.

diff -r 3d10de7a8ca7 -r ac90764bb654 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Mar 15 17:59:33 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Mar 16 20:19:25 2006 +0100
@@ -47,6 +47,8 @@
 
   val parameters_of: theory -> string ->
     ((string * typ) * mixfix) list
+  val parameters_of_expr: theory -> expr ->
+    ((string * typ) * mixfix) list
   val local_asms_of: theory -> string ->
     ((string * Attrib.src list) * term list) list
   val global_asms_of: theory -> string ->
@@ -1275,6 +1277,14 @@
 fun parameters_of thy name =
   the_locale thy name |> #params |> fst;
 
+fun parameters_of_expr thy expr =
+  let
+    val ctxt = ProofContext.init thy;
+    val ((_, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
+        (([], Symtab.empty), Expr expr);
+    val ((parms, _, _), _) = read_elemss false ctxt [] raw_elemss [];
+  in map (fn p as (n, _) => (p, Symtab.lookup syn n |> the)) parms end;
+
 fun local_asms_of thy name =
   gen_asms_of (single o Library.last_elem) thy name;