src/Pure/defs.ML
changeset 16838 131ca99f6abf
parent 16826 ed53f24149f6
child 16877 e92cba1d4842
     1.1 --- a/src/Pure/defs.ML	Thu Jul 14 19:28:19 2005 +0200
     1.2 +++ b/src/Pure/defs.ML	Thu Jul 14 19:28:20 2005 +0200
     1.3 @@ -197,8 +197,6 @@
     1.4        NONE => false
     1.5      | _ => true
     1.6             
     1.7 -structure Inttab = TableFun(type key = int val ord = int_ord);
     1.8 -
     1.9  fun normalize_edge_idx (edge as (maxidx, u1, v1, history)) =
    1.10      if maxidx <= 1000000 then edge else
    1.11      let