src/Tools/Compute_Oracle/linker.ML
changeset 26343 0dd2eab7b296
parent 26336 a0e2b706ce73
child 29269 5c25a2012975
     1.1 --- a/src/Tools/Compute_Oracle/linker.ML	Wed Mar 19 22:50:42 2008 +0100
     1.2 +++ b/src/Tools/Compute_Oracle/linker.ML	Thu Mar 20 00:20:44 2008 +0100
     1.3 @@ -192,7 +192,7 @@
     1.4  fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs
     1.5  
     1.6  local
     1.7 -    fun get_thm thmname = PureThy.get_thm (theory "Main") (Facts.Named (thmname, NONE))
     1.8 +    fun get_thm thmname = PureThy.get_thm (theory "Main") thmname
     1.9      val eq_th = get_thm "HOL.eq_reflection"
    1.10  in
    1.11    fun eq_to_meta th = (eq_th OF [th] handle THM _ => th)