Replaced quote by Library.quote, since quote now refers to Symbol.quote
authorberghofe
Fri Apr 16 18:55:25 2004 +0200 (2004-04-16)
changeset 14601e46e7cdcf796
parent 14600 ba51bc239716
child 14602 e06ded775eca
Replaced quote by Library.quote, since quote now refers to Symbol.quote
src/HOLCF/domain/interface.ML
     1.1 --- a/src/HOLCF/domain/interface.ML	Fri Apr 16 18:48:13 2004 +0200
     1.2 +++ b/src/HOLCF/domain/interface.ML	Fri Apr 16 18:55:25 2004 +0200
     1.3 @@ -13,10 +13,10 @@
     1.4  
     1.5  (* --- generation of bindings for axioms and theorems in .thy.ML - *)
     1.6  
     1.7 -  fun get      dname name   = "get_thm thy " ^ quote (dname^"."^name);
     1.8 +  fun get      dname name   = "get_thm thy " ^ Library.quote (dname^"."^name);
     1.9    fun gen_vals dname name   = "val "^ name ^ " = get_thm" ^ 
    1.10  			(if hd (rev (Symbol.explode name)) = "s" then "s" else "")^
    1.11 -			" thy " ^ quote (dname^"."^name)^";";
    1.12 +			" thy " ^ Library.quote (dname^"."^name)^";";
    1.13    fun gen_vall       name l = "val "^name^" = "^ mk_list l^";";
    1.14    val rews = "iso_rews @ when_rews @\n\
    1.15   	   \  con_rews @ sel_rews @ dis_rews @ dist_les @ dist_eqs @\n\
    1.16 @@ -63,11 +63,11 @@
    1.17      val thy_ext_string = let
    1.18        fun mk_conslist cons' = 
    1.19  	  mk_list (map (fn (c,syn,ts)=> "\n"^
    1.20 -		    mk_triple(quote c, syn, mk_list (map (fn (b,s ,tp) =>
    1.21 -		    mk_triple(Bool.toString b, quote s, tp)) ts))) cons');
    1.22 +		    mk_triple(Library.quote c, syn, mk_list (map (fn (b,s ,tp) =>
    1.23 +		    mk_triple(Bool.toString b, Library.quote s, tp)) ts))) cons');
    1.24      in "val thy = thy |> Domain_Extender.add_domain "
    1.25 -       ^ mk_pair(quote comp_dname, mk_list(map (fn ((n,vs),cs) => "\n"^
    1.26 -				   mk_pair (mk_pair (quote n, mk_list vs), 
    1.27 +       ^ mk_pair(Library.quote comp_dname, mk_list(map (fn ((n,vs),cs) => "\n"^
    1.28 +				   mk_pair (mk_pair (Library.quote n, mk_list vs), 
    1.29  					    mk_conslist cs)) eqs'))
    1.30         ^ ";\n"
    1.31      end;
    1.32 @@ -112,7 +112,7 @@
    1.33  			|   esc (x   ::xs) = x  ::esc xs
    1.34  		    in implode (esc (Symbol.explode s)) end;
    1.35    val type_var' = ((type_var >> unenclose) ^^ 
    1.36 -	          optional ($$ "::" ^^ !! (sort >> esc_quote)) "") >> quote;
    1.37 +	          optional ($$ "::" ^^ !! (sort >> esc_quote)) "") >> Library.quote;
    1.38    val type_args = (type_var' >> single
    1.39                   ||  "(" $$-- !! (list1 type_var' --$$ ")")
    1.40                   ||  empty >> K [])