author | wenzelm |
Sun, 09 Mar 2014 17:07:45 +0100 | |
changeset 56004 | 0364adabdc7b |
parent 56003 | eccac152ffb4 |
child 56005 | 4f4fc80b0613 |
src/Pure/facts.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/facts.ML Sun Mar 09 17:02:18 2014 +0100 +++ b/src/Pure/facts.ML Sun Mar 09 17:07:45 2014 +0100 @@ -86,9 +86,6 @@ fun pos_of_ref (Named ((_, pos), _)) = pos | pos_of_ref (Fact _) = Position.none; -fun name_pos_of_ref (Named (name_pos, _)) = name_pos - | name_pos_of_ref (Fact _) = raise Fail "Illegal literal fact"; - fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is) | map_name_of_ref _ r = r;