src/HOL/Tools/Function/termination.ML
changeset 37678 0040bafffdef
parent 37391 476270a6c2dc
child 38549 d0385f2764d8
     1.1 --- a/src/HOL/Tools/Function/termination.ML	Thu Jul 01 16:54:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/Function/termination.ML	Thu Jul 01 16:54:44 2010 +0200
     1.3 @@ -106,7 +106,7 @@
     1.4    end
     1.5  
     1.6  (* compute list of types for nodes *)
     1.7 -fun node_types sk T = dest_tree (fn Type (@{type_name "+"}, [LT, RT]) => (LT, RT)) sk T |> map snd
     1.8 +fun node_types sk T = dest_tree (fn Type (@{type_name Sum_Type.sum}, [LT, RT]) => (LT, RT)) sk T |> map snd
     1.9  
    1.10  (* find index and raw term *)
    1.11  fun dest_inj (SLeaf i) trm = (i, trm)