# HG changeset patch
# User desharna
# Date 1740737593 -3600
# Node ID 4a21e6973e1133a456cf5bc9c9c93166f39e1891
# Parent  559399b4de9f0d874ce2f779ff914facf27f4492
added type names and type annotations

diff -r 559399b4de9f -r 4a21e6973e11 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Fri Feb 28 10:42:40 2025 +0100
+++ b/src/HOL/Tools/try0.ML	Fri Feb 28 11:13:13 2025 +0100
@@ -9,9 +9,10 @@
   val noneN : string
   val silence_methods : bool -> Proof.context -> Proof.context
   datatype modifier = Use | Simp | Intro | Elim | Dest
+  type xthm = Facts.ref * Token.src list
+  type tagged_xthm = xthm * modifier list
   type result = {name: string, command: string, time: Time.time, state: Proof.state}
-  val try0 : Time.time option -> ((Facts.ref * Token.src list)  * modifier list) list ->
-    Proof.state -> result list
+  val try0 : Time.time option -> tagged_xthm list -> Proof.state -> result list
 end
 
 structure Try0 : TRY0 =
@@ -46,20 +47,22 @@
   |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source")
 
 datatype modifier = Use | Simp | Intro | Elim | Dest
+type xthm = Facts.ref * Token.src list
+type tagged_xthm = xthm * modifier list
 
-fun string_of_xthm (xref, args) =
+fun string_of_xthm ((xref, args) : xthm) =
   (case xref of
     Facts.Fact literal => literal |> Symbol_Pos.explode0 |> Symbol_Pos.implode |> cartouche
   | _ =>
       Facts.string_of_ref xref) ^ implode
         (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args)
 
-fun add_attr_text tagged (tag, src) s =
+fun add_attr_text (tagged : tagged_xthm list) (tag, src) s =
   let
     val fs = tagged |> filter (fn (_, tags) => member (op =) tags tag) |> map (string_of_xthm o fst)
   in if null fs then s else s ^ " " ^ (if src = "" then "" else src ^ ": ") ^ implode_space fs end
 
-fun attrs_text tags tagged =
+fun attrs_text tags (tagged : tagged_xthm list) =
   "" |> fold (add_attr_text tagged) tags
 
 type result = {name: string, command: string, time: Time.time, state: Proof.state}
@@ -145,7 +148,7 @@
       |> Config.put Unify.unify_trace false
       |> Config.put Argo_Tactic.trace "none")
 
-fun generic_try0 mode timeout_opt tagged st =
+fun generic_try0 mode timeout_opt (tagged : tagged_xthm list) st =
   let
     val st = Proof.map_contexts (silence_methods false) st
     fun try_method method = method mode timeout_opt tagged st