1 fun t_foo bar = bar
2
3 structure TStruct =
4 struct
5 fun ts_foo bar = bar;
6 end;
7
8 @{thm refl};
9 (*@{thm ta_foo}; *** (ta_foo) has not been declared*)