src/Pure/zterm.ML

           (ZAppt (proof p, Same.commit term t)
             handle Same.SAME => ZAppt (p, term t))
       | proof (ZAppp (p, q)) =
           (ZAppp (proof p, Same.commit proof q)
             handle Same.SAME => ZAppp (p, proof q))
-      | proof (ZClassp (T, c)) = ZClassp (typ T, c);
+      | proof (ZClassp (T, c)) = if hyps then ZClassp (typ T, c) else raise Same.SAME;
   in proof end;
 
 fun map_proof hyps typ term = Same.commit (map_proof_same hyps typ term);
 fun map_proof_types hyps typ = map_proof hyps typ (subst_term_same typ Same.same);