src/Pure/Isar/proof_context.ML
changeset 27264 843472ae2116
parent 27259 6e71abb8c994
child 27286 2ea20e5fdf16
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Jun 18 22:32:02 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Jun 18 22:32:03 2008 +0200
     1.3 @@ -579,8 +579,7 @@
     1.4    let val Mode {pattern, ...} = get_mode ctxt in
     1.5      TypeInfer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
     1.6        (try (Consts.the_constraint (consts_of ctxt))) (Variable.def_type ctxt pattern)
     1.7 -      (Variable.names_of ctxt) (Variable.maxidx_of ctxt) NONE (map (rpair dummyT) ts)
     1.8 -    |> #1 |> map #1
     1.9 +      (Variable.names_of ctxt) (Variable.maxidx_of ctxt) ts
    1.10      handle TYPE (msg, _, _) => error msg
    1.11    end;
    1.12