src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
changeset 45034 b0f61dec677a
parent 44934 2302faa4ae0e
child 45301 866b075aa99b
equal deleted inserted replaced
45033:34e5fc15ea02 45034:b0f61dec677a
   147                     if member Thm.eq_thm_prop chained_ths th then Chained
   147                     if member Thm.eq_thm_prop chained_ths th then Chained
   148                     else General), th) :: rest))
   148                     else General), th) :: rest))
   149     |> snd
   149     |> snd
   150   end
   150   end
   151 
   151 
   152 (* This is a terrible hack. Free variables are sometimes code as "M__" when they
   152 (* This is a terrible hack. Free variables are sometimes coded as "M__" when
   153    are displayed as "M" and we want to avoid clashes with these. But sometimes
   153    they are displayed as "M" and we want to avoid clashes with these. But
   154    it's even worse: "Ma__" encodes "M". So we simply reserve all prefixes of all
   154    sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all
   155    free variables. In the worse case scenario, where the fact won't be resolved
   155    prefixes of all free variables. In the worse case scenario, where the fact
   156    correctly, the user can fix it manually, e.g., by naming the fact in
   156    won't be resolved correctly, the user can fix it manually, e.g., by naming
   157    question. Ideally we would need nothing of it, but backticks just don't work
   157    the fact in question. Ideally we would need nothing of it, but backticks
   158    with schematic variables. *)
   158    simply don't work with schematic variables. *)
   159 fun all_prefixes_of s =
   159 fun all_prefixes_of s =
   160   map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
   160   map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
   161 fun close_form t =
   161 fun close_form t =
   162   (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
   162   (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
   163   |> fold (fn ((s, i), T) => fn (t', taken) =>
   163   |> fold (fn ((s, i), T) => fn (t', taken) =>