diff -r 0e8e662013f9 -r 4baa475a51e6 src/HOL/Proofs/Extraction/Higman_Extraction.thy
--- a/src/HOL/Proofs/Extraction/Higman_Extraction.thy	Tue Oct 18 15:40:59 2011 +0200
+++ b/src/HOL/Proofs/Extraction/Higman_Extraction.thy	Wed Oct 19 08:37:14 2011 +0200
@@ -107,58 +107,4 @@
 end;
 *}
 
-text {* The same story with the legacy SML code generator,
-this can be removed once the code generator is removed. *}
-
-code_module Higman
-contains
-  higman = higman_idx
-
-ML {*
-local open Higman in
-
-val a = 16807.0;
-val m = 2147483647.0;
-
-fun nextRand seed =
-  let val t = a*seed
-  in  t - m * real (Real.floor(t/m)) end;
-
-fun mk_word seed l =
-  let
-    val r = nextRand seed;
-    val i = Real.round (r / m * 10.0);
-  in if i > 7 andalso l > 2 then (r, []) else
-    apsnd (cons (if i mod 2 = 0 then A else B)) (mk_word r (l+1))
-  end;
-
-fun f s zero = mk_word s 0
-  | f s (Suc n) = f (fst (mk_word s 0)) n;
-
-val g1 = snd o (f 20000.0);
-
-val g2 = snd o (f 50000.0);
-
-fun f1 zero = [A,A]
-  | f1 (Suc zero) = [B]
-  | f1 (Suc (Suc zero)) = [A,B]
-  | f1 _ = [];
-
-fun f2 zero = [A,A]
-  | f2 (Suc zero) = [B]
-  | f2 (Suc (Suc zero)) = [B,A]
-  | f2 _ = [];
-
-val (i1, j1) = higman g1;
-val (v1, w1) = (g1 i1, g1 j1);
-val (i2, j2) = higman g2;
-val (v2, w2) = (g2 i2, g2 j2);
-val (i3, j3) = higman f1;
-val (v3, w3) = (f1 i3, f1 j3);
-val (i4, j4) = higman f2;
-val (v4, w4) = (f2 i4, f2 j4);
-
-end;
-*}
-
 end