| changeset 57942 | e5bec882fdd0 |
| parent 57929 | c5063c033a5a |
| child 61054 | add998b3c597 |
--- a/src/Pure/global_theory.ML Thu Aug 14 14:28:11 2014 +0200 +++ b/src/Pure/global_theory.ML Thu Aug 14 16:20:14 2014 +0200 @@ -72,7 +72,7 @@ (* retrieve theorems *) fun get_thms thy xname = - #2 (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none)); + #thms (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none)); fun get_thm thy xname = Facts.the_single (xname, Position.none) (get_thms thy xname);