src/HOL/UNITY/PPROD.ML

 \       OK I (%i. lift i (F i)) |]  \
 \    ==> (PLam I F) : X guarantees Y"; 
 by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
 qed "guarantees_PLam_I";
 
-Goal "Allowed (PLam I F) = (INT i:I. lift i `` Allowed(F i))";
+Goal "Allowed (PLam I F) = (INT i:I. lift i ` Allowed(F i))";
 by (simp_tac (simpset() addsimps [PLam_def]) 1); 
 qed "Allowed_PLam";
 Addsimps [Allowed_PLam];
 
 Goal "(PLam I F) : preserves v = (ALL i:I. F i : preserves (v o lift_map i))";