src/CCL/wfd.ML

 
 goalw Wfd.thy [NatPR_def]  "p : NatPR <-> (EX x:Nat.p=<x,succ(x)>)";
 by (fast_tac set_cs 1);
 val NatPRXH = result();
 
-goalw Wfd.thy [ListPR_def]  "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h.t>)";
+goalw Wfd.thy [ListPR_def]  "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h$t>)";
 by (fast_tac set_cs 1);
 val ListPRXH = result();
 
 val NatPRI = refl RS (bexI RS (NatPRXH RS iffD2));
 val ListPRI = refl RS (bexI RS (bexI RS (ListPRXH RS iffD2)));