# HG changeset patch
# User berghofe
# Date 1082134525 -7200
# Node ID e46e7cdcf7960e6caf5b6597743f3f571ff5876a
# Parent  ba51bc23971607aa983dd793ee34005dfb5fc970
Replaced quote by Library.quote, since quote now refers to Symbol.quote

diff -r ba51bc239716 -r e46e7cdcf796 src/HOLCF/domain/interface.ML
--- a/src/HOLCF/domain/interface.ML	Fri Apr 16 18:48:13 2004 +0200
+++ b/src/HOLCF/domain/interface.ML	Fri Apr 16 18:55:25 2004 +0200
@@ -13,10 +13,10 @@
 
 (* --- generation of bindings for axioms and theorems in .thy.ML - *)
 
-  fun get      dname name   = "get_thm thy " ^ quote (dname^"."^name);
+  fun get      dname name   = "get_thm thy " ^ Library.quote (dname^"."^name);
   fun gen_vals dname name   = "val "^ name ^ " = get_thm" ^ 
 			(if hd (rev (Symbol.explode name)) = "s" then "s" else "")^
-			" thy " ^ quote (dname^"."^name)^";";
+			" thy " ^ Library.quote (dname^"."^name)^";";
   fun gen_vall       name l = "val "^name^" = "^ mk_list l^";";
   val rews = "iso_rews @ when_rews @\n\
  	   \  con_rews @ sel_rews @ dis_rews @ dist_les @ dist_eqs @\n\
@@ -63,11 +63,11 @@
     val thy_ext_string = let
       fun mk_conslist cons' = 
 	  mk_list (map (fn (c,syn,ts)=> "\n"^
-		    mk_triple(quote c, syn, mk_list (map (fn (b,s ,tp) =>
-		    mk_triple(Bool.toString b, quote s, tp)) ts))) cons');
+		    mk_triple(Library.quote c, syn, mk_list (map (fn (b,s ,tp) =>
+		    mk_triple(Bool.toString b, Library.quote s, tp)) ts))) cons');
     in "val thy = thy |> Domain_Extender.add_domain "
-       ^ mk_pair(quote comp_dname, mk_list(map (fn ((n,vs),cs) => "\n"^
-				   mk_pair (mk_pair (quote n, mk_list vs), 
+       ^ mk_pair(Library.quote comp_dname, mk_list(map (fn ((n,vs),cs) => "\n"^
+				   mk_pair (mk_pair (Library.quote n, mk_list vs), 
 					    mk_conslist cs)) eqs'))
        ^ ";\n"
     end;
@@ -112,7 +112,7 @@
 			|   esc (x   ::xs) = x  ::esc xs
 		    in implode (esc (Symbol.explode s)) end;
   val type_var' = ((type_var >> unenclose) ^^ 
-	          optional ($$ "::" ^^ !! (sort >> esc_quote)) "") >> quote;
+	          optional ($$ "::" ^^ !! (sort >> esc_quote)) "") >> Library.quote;
   val type_args = (type_var' >> single
                  ||  "(" $$-- !! (list1 type_var' --$$ ")")
                  ||  empty >> K [])