fix: common constraints;
authorwenzelm
Wed Sep 01 21:10:05 1999 +0200 (1999-09-01)
changeset 74114dbff71ac480
parent 7410 7369a35fb3c2
child 7412 35ebe1452c10
fix: common constraints;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Sep 01 21:09:10 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Sep 01 21:10:05 1999 +0200
     1.3 @@ -56,8 +56,8 @@
     1.4    val assume_i: ((int -> tactic) * (int -> tactic))
     1.5      -> (string * context attribute list * (term * (term list * term list)) list) list
     1.6      -> context -> context * ((string * thm list) list * thm list)
     1.7 -  val fix: (string * string option) list -> context -> context
     1.8 -  val fix_i: (string * typ) list -> context -> context
     1.9 +  val fix: (string list * string option) list -> context -> context
    1.10 +  val fix_i: (string list * typ) list -> context -> context
    1.11    val transfer_used_names: context -> context -> context
    1.12    val setup: (theory -> theory) list
    1.13  end;
    1.14 @@ -714,7 +714,8 @@
    1.15          (thy, data, (assumes, ((x, Syntax.skolem x') :: fixes, x' :: names)), binds, thms, defs)
    1.16        end);
    1.17  
    1.18 -fun gen_fixs prep check xs ctxt = foldl (gen_fix prep check) (ctxt, xs);
    1.19 +fun gen_fixs prep check vars ctxt =
    1.20 +  foldl (gen_fix prep check) (ctxt, flat (map (fn (xs, T) => map (rpair T) xs) vars));
    1.21  
    1.22  
    1.23  val fix = gen_fixs read_skolemT true;