src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
changeset 55205 8450622db0c5
parent 55202 824c48a539c9
child 55212 5832470d956e
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Fri Jan 31 10:34:20 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Fri Jan 31 12:30:54 2014 +0100
     1.3 @@ -130,7 +130,6 @@
     1.4      (t', subst)
     1.5    end
     1.6  
     1.7 -
     1.8  (* (4) Typing-spot table *)
     1.9  local
    1.10  fun key_of_atype (TVar (z, _)) = Ord_List.insert indexname_ord z