author | wenzelm |
Fri, 31 Oct 1997 15:19:50 +0100 | |
changeset 4052 | 026069ba0316 |
parent 4051 | 6b72919c9b4b |
child 4053 | c88d0d5ae806 |
src/Pure/sign.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/sign.ML Fri Oct 31 15:15:06 1997 +0100 +++ b/src/Pure/sign.ML Fri Oct 31 15:19:50 1997 +0100 @@ -171,7 +171,7 @@ (* data *) -fun access_data f sg = f (#data (rep_sg sg)) +fun access_data f sg k = f (#data (rep_sg sg)) k handle ERROR => error ("of theory " ^ str_of_sg sg); val get_data = access_data Data.get;