changeset 33955 | fff6f11b1f09 |
parent 33522 | 737589bb9bb8 |
child 35021 | c839a4c670c6 |
--- a/src/HOL/Import/hol4rews.ML Tue Nov 24 14:37:23 2009 +0100 +++ b/src/HOL/Import/hol4rews.ML Tue Nov 24 17:28:25 2009 +0100 @@ -480,7 +480,7 @@ then let val paths = Long_Name.explode isa - val i = Library.drop(length paths - 2,paths) + val i = drop (length paths - 2) paths in case i of [seg,con] => output_thy ^ "." ^ seg ^ "." ^ con