# HG changeset patch
# User haftmann
# Date 1319058468 -7200
# Node ID 3dd426ae6bead211586ad056807a382434c8d26b
# Parent  b416573f18077346667a074234eaa337dbd9b891
removed some remaining artefacts of ancient SML code generator

diff -r b416573f1807 -r 3dd426ae6bea doc-src/Codegen/Thy/Foundations.thy
--- a/doc-src/Codegen/Thy/Foundations.thy	Wed Oct 19 22:54:26 2011 +0200
+++ b/doc-src/Codegen/Thy/Foundations.thy	Wed Oct 19 23:07:48 2011 +0200
@@ -125,12 +125,6 @@
   code_thms} (see \secref{sec:equations}) provides a convenient
   mechanism to inspect the impact of a preprocessor setup on code
   equations.
-
-  \begin{warn}
-    Attribute @{attribute code_unfold} also applies to the
-    preprocessor of the ancient @{text "SML code generator"}; in case
-    this is not what you intend, use @{attribute code_inline} instead.
-  \end{warn}
 *}
 
 
diff -r b416573f1807 -r 3dd426ae6bea doc-src/Codegen/Thy/Introduction.thy
--- a/doc-src/Codegen/Thy/Introduction.thy	Wed Oct 19 22:54:26 2011 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy	Wed Oct 19 23:07:48 2011 +0200
@@ -236,15 +236,6 @@
     \begin{center}\textit{Happy proving, happy hacking!}\end{center}
 
   \end{minipage}}}\end{center}
-
-  \begin{warn}
-    There is also a more ancient code generator in Isabelle by Stefan
-    Berghofer \cite{Berghofer-Nipkow:2002}.  Although its
-    functionality is covered by the code generator presented here, it
-    will sometimes show up as an artifact.  In case of ambiguity, we
-    will refer to the framework described here as @{text "generic code
-    generator"}, to the other as @{text "SML code generator"}.
-  \end{warn}
 *}
 
 end
diff -r b416573f1807 -r 3dd426ae6bea doc-src/Codegen/Thy/document/Foundations.tex
--- a/doc-src/Codegen/Thy/document/Foundations.tex	Wed Oct 19 22:54:26 2011 +0200
+++ b/doc-src/Codegen/Thy/document/Foundations.tex	Wed Oct 19 23:07:48 2011 +0200
@@ -184,13 +184,7 @@
   \noindent The current setup of the preprocessor may be inspected
   using the \indexdef{}{command}{print\_codeproc}\hypertarget{command.print-codeproc}{\hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codeproc}}}}} command.  \indexdef{}{command}{code\_thms}\hypertarget{command.code-thms}{\hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}}} (see \secref{sec:equations}) provides a convenient
   mechanism to inspect the impact of a preprocessor setup on code
-  equations.
-
-  \begin{warn}
-    Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}unfold}}} also applies to the
-    preprocessor of the ancient \isa{SML\ code\ generator}; in case
-    this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}} instead.
-  \end{warn}%
+  equations.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r b416573f1807 -r 3dd426ae6bea doc-src/Codegen/Thy/document/Introduction.tex
--- a/doc-src/Codegen/Thy/document/Introduction.tex	Wed Oct 19 22:54:26 2011 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex	Wed Oct 19 23:07:48 2011 +0200
@@ -560,15 +560,7 @@
 
     \begin{center}\textit{Happy proving, happy hacking!}\end{center}
 
-  \end{minipage}}}\end{center}
-
-  \begin{warn}
-    There is also a more ancient code generator in Isabelle by Stefan
-    Berghofer \cite{Berghofer-Nipkow:2002}.  Although its
-    functionality is covered by the code generator presented here, it
-    will sometimes show up as an artifact.  In case of ambiguity, we
-    will refer to the framework described here as \isa{generic\ code\ generator}, to the other as \isa{SML\ code\ generator}.
-  \end{warn}%
+  \end{minipage}}}\end{center}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r b416573f1807 -r 3dd426ae6bea src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Oct 19 22:54:26 2011 +0200
+++ b/src/Pure/Isar/code.ML	Wed Oct 19 23:07:48 2011 +0200
@@ -76,9 +76,6 @@
   val get_case_cong: theory -> string -> thm option
   val undefineds: theory -> string list
   val print_codesetup: theory -> unit
-
-  (*infrastructure*)
-  val set_code_target_attr: (string -> thm -> theory -> theory) -> theory -> theory
 end;
 
 signature CODE_DATA_ARGS =
@@ -1264,26 +1261,6 @@
   end;
 
 
-(** infrastructure **)
-
-(* cf. src/HOL/Tools/recfun_codegen.ML *)
-
-structure Code_Target_Attr = Theory_Data
-(
-  type T = (string -> thm -> theory -> theory) option;
-  val empty = NONE;
-  val extend = I;
-  val merge = merge_options;
-);
-
-fun set_code_target_attr f = Code_Target_Attr.map (K (SOME f));
-
-fun code_target_attr prefix thm thy =
-  let
-    val attr = the_default ((K o K) I) (Code_Target_Attr.get thy);
-  in thy |> add_warning_eqn thm |> attr prefix thm end;
-
-
 (* setup *)
 
 val _ = Context.>> (Context.map_theory
@@ -1294,8 +1271,6 @@
       || Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn)
       || Args.$$$ "abstype" |-- Scan.succeed (mk_attribute add_abstype)
       || Args.$$$ "abstract" |-- Scan.succeed (mk_attribute add_abs_eqn)
-      || (Args.$$$ "target" |-- Args.colon |-- Args.name >>
-           (mk_attribute o code_target_attr))
       || Scan.succeed (mk_attribute add_warning_eqn);
   in
     Datatype_Interpretation.init