src/Tools/Compute_Oracle/linker.ML
changeset 37869 e9c6a7fe1989
parent 37863 7f113caabcf4
equal deleted inserted replaced
37868:59eed00bfd8e 37869:e9c6a7fe1989
   188         (added_substs, Instances (cfilter, ctab, minsets, substs))
   188         (added_substs, Instances (cfilter, ctab, minsets, substs))
   189     end
   189     end
   190 
   190 
   191 fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs
   191 fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs
   192 
   192 
   193 local
   193 fun eq_to_meta th = (@{thm HOL.eq_reflection} OF [th] handle THM _ => th)
   194     fun get_thm thmname = PureThy.get_thm @{theory Main} thmname
       
   195     val eq_th = get_thm "HOL.eq_reflection"
       
   196 in
       
   197   fun eq_to_meta th = (eq_th OF [th] handle THM _ => th)
       
   198 end
       
   199 
   194 
   200 
   195 
   201 local
   196 local
   202 
   197 
   203 fun collect (Var x) tab = tab
   198 fun collect (Var x) tab = tab