--- 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 [])