removing old code generator setup for function types
authorbulwahn
Wed Oct 19 08:37:20 2011 +0200 (2011-10-19)
changeset 4517410c3597f92f0
parent 45173 81a3fb857ab8
child 45175 ae8411edd939
removing old code generator setup for function types
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Fun.thy	Wed Oct 19 08:37:19 2011 +0200
     1.2 +++ b/src/HOL/Fun.thy	Wed Oct 19 08:37:20 2011 +0200
     1.3 @@ -812,28 +812,6 @@
     1.4  
     1.5  subsubsection {* Code generator *}
     1.6  
     1.7 -types_code
     1.8 -  "fun"  ("(_ ->/ _)")
     1.9 -attach (term_of) {*
    1.10 -fun term_of_fun_type _ aT _ bT _ = Free ("<function>", aT --> bT);
    1.11 -*}
    1.12 -attach (test) {*
    1.13 -fun gen_fun_type aF aT bG bT i =
    1.14 -  let
    1.15 -    val tab = Unsynchronized.ref [];
    1.16 -    fun mk_upd (x, (_, y)) t = Const ("Fun.fun_upd",
    1.17 -      (aT --> bT) --> aT --> bT --> aT --> bT) $ t $ aF x $ y ()
    1.18 -  in
    1.19 -    (fn x =>
    1.20 -       case AList.lookup op = (!tab) x of
    1.21 -         NONE =>
    1.22 -           let val p as (y, _) = bG i
    1.23 -           in (tab := (x, p) :: !tab; y) end
    1.24 -       | SOME (y, _) => y,
    1.25 -     fn () => Basics.fold mk_upd (!tab) (Const ("HOL.undefined", aT --> bT)))
    1.26 -  end;
    1.27 -*}
    1.28 -
    1.29  code_const "op \<circ>"
    1.30    (SML infixl 5 "o")
    1.31    (Haskell infixr 9 ".")