# HG changeset patch
# User bulwahn
# Date 1319006240 -7200
# Node ID 10c3597f92f0bd857a398cf1ad6d134a8f669852
# Parent  81a3fb857ab8ba6f4bf063c55c1d6deee490f444
removing old code generator setup for function types

diff -r 81a3fb857ab8 -r 10c3597f92f0 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Wed Oct 19 08:37:19 2011 +0200
+++ b/src/HOL/Fun.thy	Wed Oct 19 08:37:20 2011 +0200
@@ -812,28 +812,6 @@
 
 subsubsection {* Code generator *}
 
-types_code
-  "fun"  ("(_ ->/ _)")
-attach (term_of) {*
-fun term_of_fun_type _ aT _ bT _ = Free ("<function>", aT --> bT);
-*}
-attach (test) {*
-fun gen_fun_type aF aT bG bT i =
-  let
-    val tab = Unsynchronized.ref [];
-    fun mk_upd (x, (_, y)) t = Const ("Fun.fun_upd",
-      (aT --> bT) --> aT --> bT --> aT --> bT) $ t $ aF x $ y ()
-  in
-    (fn x =>
-       case AList.lookup op = (!tab) x of
-         NONE =>
-           let val p as (y, _) = bG i
-           in (tab := (x, p) :: !tab; y) end
-       | SOME (y, _) => y,
-     fn () => Basics.fold mk_upd (!tab) (Const ("HOL.undefined", aT --> bT)))
-  end;
-*}
-
 code_const "op \<circ>"
   (SML infixl 5 "o")
   (Haskell infixr 9 ".")