# HG changeset patch
# User wenzelm
# Date 936213005 -7200
# Node ID 4dbff71ac48035db66c7dc8c492a829438d9855a
# Parent  7369a35fb3c28bdebb82aabc0a10794f6159321e
fix: common constraints;

diff -r 7369a35fb3c2 -r 4dbff71ac480 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Sep 01 21:09:10 1999 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Sep 01 21:10:05 1999 +0200
@@ -56,8 +56,8 @@
   val assume_i: ((int -> tactic) * (int -> tactic))
     -> (string * context attribute list * (term * (term list * term list)) list) list
     -> context -> context * ((string * thm list) list * thm list)
-  val fix: (string * string option) list -> context -> context
-  val fix_i: (string * typ) list -> context -> context
+  val fix: (string list * string option) list -> context -> context
+  val fix_i: (string list * typ) list -> context -> context
   val transfer_used_names: context -> context -> context
   val setup: (theory -> theory) list
 end;
@@ -714,7 +714,8 @@
         (thy, data, (assumes, ((x, Syntax.skolem x') :: fixes, x' :: names)), binds, thms, defs)
       end);
 
-fun gen_fixs prep check xs ctxt = foldl (gen_fix prep check) (ctxt, xs);
+fun gen_fixs prep check vars ctxt =
+  foldl (gen_fix prep check) (ctxt, flat (map (fn (xs, T) => map (rpair T) xs) vars));
 
 
 val fix = gen_fixs read_skolemT true;