adapt to Lean changes

leanprover-community · Aug 23, 2017 · d708489 · d708489
1 parent 3d81768
commit d708489
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/set_theory.lean b/theories/set_theory.lean
@@ -181,7 +181,7 @@ namespace pSet
 
     def eval (n) : resp n → arity Set.{u} n := eval_aux.1
 
-    @[simp] def eval_val {n f x} : (@eval (n+1) f : Set → arity Set n) ⟦x⟧ = eval n (f.f x) := rfl
+    @[simp] def eval_val {n f x} : (@eval (n+1) f : Set → arity Set n) ⟦x⟧ = eval n (resp.f f x) := rfl
   end resp
 
   inductive definable (n) : arity Set.{u} n → Type (u+1)