Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/domain/interface.ML
changeset 16486 1a12cdb6ee6b
parent 16394 495dbcd4f4c9 
--- a/src/HOLCF/domain/interface.ML	Mon Jun 20 22:13:58 2005 +0200
+++ b/src/HOLCF/domain/interface.ML	Mon Jun 20 22:13:59 2005 +0200
@@ -12,10 +12,10 @@
 
 (* --- generation of bindings for axioms and theorems in .thy.ML - *)
 
-  fun get      dname name   = "get_thm thy (" ^ Library.quote (dname ^ "." ^ name) ^ ", NONE)";
+  fun get      dname name   = "get_thm thy (PureThy.Name " ^ Library.quote (dname ^ "." ^ name) ^ ")";
   fun gen_vals dname name   = "val "^ name ^ " = get_thm" ^ 
 			(if hd (rev (Symbol.explode name)) = "s" then "s" else "")^
-			" thy (" ^ Library.quote (dname ^ "." ^ name) ^ ", NONE);";
+			" thy (PureThy.Name " ^ 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\
isabelle