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/Pure/codegen.ML
changeset 44052 00f0c8782a51
parent 43956 4611af362cd0 
--- a/src/Pure/codegen.ML	Mon Aug 08 13:19:19 2011 +0200
+++ b/src/Pure/codegen.ML	Mon Aug 08 13:29:54 2011 +0200
@@ -916,7 +916,9 @@
 
 fun eval_term ctxt t =
   let
-    val _ = legacy_feature "Old evaluation mechanism -- use evaluator 'code' or method eval instead";
+    val _ =
+      legacy_feature
+        "Old evaluation mechanism -- use evaluator \"code\" or method \"eval\" instead";
     val thy = Proof_Context.theory_of ctxt;
     val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
       error "Term to be evaluated contains type variables";
@@ -1013,7 +1015,7 @@
    || Scan.repeat1 (Parse.term >> pair "")) >>
   (fn ((((mode, module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
     let
-      val _ = legacy_feature "Old code generation command -- use export_code instead";
+      val _ = legacy_feature "Old code generation command -- use 'export_code' instead";
       val mode' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode);
       val (code, gr) = generate_code thy mode' modules module xs;
       val thy' = thy |> Context.theory_map (ML_Context.exec (fn () =>
isabelle