src/HOLCF/Tools/Domain/domain_library.ML
changeset 37391 476270a6c2dc
parent 37145 01aa36932739
child 38549 d0385f2764d8
--- a/src/HOLCF/Tools/Domain/domain_library.ML	Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_library.ML	Thu Jun 10 12:24:03 2010 +0200
@@ -215,7 +215,7 @@
   | prj _  _  _ []         _ = raise Fail "Domain_Library.prj: empty list"
   | prj f1 _  x (_::y::ys) 0 = f1 x y
   | prj f1 f2 x (y::   ys) j = prj f1 f2 (f2 x y) ys (j-1);
-fun  proj x      = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
+fun proj x = prj (fn S => K (%%: @{const_name fst} $ S)) (fn S => K (%%: @{const_name snd} $ S)) x;
 fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
 
 val UU = %%: @{const_name UU};