src/HOL/Tools/Sledgehammer/metis_tactics.ML

 
 fun smart_invert_const "fequal" = @{const_name "op ="}
   | smart_invert_const s = invert_const s
 
 fun hol_type_from_metis_term _ (Metis.Term.Var v) =
-     (case strip_prefix_and_undo_ascii tvar_prefix v of
+     (case strip_prefix_and_unascii tvar_prefix v of
           SOME w => make_tvar w
         | NONE   => make_tvar v)
   | hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) =
-     (case strip_prefix_and_undo_ascii type_const_prefix x of
+     (case strip_prefix_and_unascii type_const_prefix x of
           SOME tc => Term.Type (smart_invert_const tc,
                                 map (hol_type_from_metis_term ctxt) tys)
         | NONE    =>
-      case strip_prefix_and_undo_ascii tfree_prefix x of
+      case strip_prefix_and_unascii tfree_prefix x of
           SOME tf => mk_tfree ctxt tf
         | NONE    => raise Fail ("hol_type_from_metis_term: " ^ x));
 
 (*Maps metis terms to isabelle terms*)
 fun hol_term_from_metis_PT ctxt fol_tm =
   let val thy = ProofContext.theory_of ctxt
       val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
                                   Metis.Term.toString fol_tm)
       fun tm_to_tt (Metis.Term.Var v) =
-             (case strip_prefix_and_undo_ascii tvar_prefix v of
+             (case strip_prefix_and_unascii tvar_prefix v of
                   SOME w => Type (make_tvar w)
                 | NONE =>
-              case strip_prefix_and_undo_ascii schematic_var_prefix v of
+              case strip_prefix_and_unascii schematic_var_prefix v of
                   SOME w => Term (mk_var (w, HOLogic.typeT))
                 | NONE   => Term (mk_var (v, HOLogic.typeT)) )
                     (*Var from Metis with a name like _nnn; possibly a type variable*)
         | tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg   (*hBOOL*)
         | tm_to_tt (t as Metis.Term.Fn (".",_)) =

             end
         | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
       and applic_to_tt ("=",ts) =
             Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
         | applic_to_tt (a,ts) =
-            case strip_prefix_and_undo_ascii const_prefix a of
+            case strip_prefix_and_unascii const_prefix a of
                 SOME b =>
                   let val c = smart_invert_const b
                       val ntypes = num_type_args thy c
                       val nterms = length ts - ntypes
                       val tts = map tm_to_tt ts

                                    cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
                                    " the terms are \n" ^
                                    cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
                      end
               | NONE => (*Not a constant. Is it a type constructor?*)
-            case strip_prefix_and_undo_ascii type_const_prefix a of
+            case strip_prefix_and_unascii type_const_prefix a of
                 SOME b =>
                   Type (Term.Type (smart_invert_const b, types_of (map tm_to_tt ts)))
               | NONE => (*Maybe a TFree. Should then check that ts=[].*)
-            case strip_prefix_and_undo_ascii tfree_prefix a of
+            case strip_prefix_and_unascii tfree_prefix a of
                 SOME b => Type (mk_tfree ctxt b)
               | NONE => (*a fixed variable? They are Skolem functions.*)
-            case strip_prefix_and_undo_ascii fixed_var_prefix a of
+            case strip_prefix_and_unascii fixed_var_prefix a of
                 SOME b =>
                   let val opr = Term.Free(b, HOLogic.typeT)
                   in  apply_list opr (length ts) (map tm_to_tt ts)  end
               | NONE => raise Fail ("unexpected metis function: " ^ a)
   in

 (*Maps fully-typed metis terms to isabelle terms*)
 fun hol_term_from_metis_FT ctxt fol_tm =
   let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
                                   Metis.Term.toString fol_tm)
       fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
-             (case strip_prefix_and_undo_ascii schematic_var_prefix v of
+             (case strip_prefix_and_unascii schematic_var_prefix v of
                   SOME w =>  mk_var(w, dummyT)
                 | NONE   => mk_var(v, dummyT))
         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
             Const (@{const_name "op ="}, HOLogic.typeT)
         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
-           (case strip_prefix_and_undo_ascii const_prefix x of
+           (case strip_prefix_and_unascii const_prefix x of
                 SOME c => Const (smart_invert_const c, dummyT)
               | NONE => (*Not a constant. Is it a fixed variable??*)
-            case strip_prefix_and_undo_ascii fixed_var_prefix x of
+            case strip_prefix_and_unascii fixed_var_prefix x of
                 SOME v => Free (v, hol_type_from_metis_term ctxt ty)
               | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
             cvt tm1 $ cvt tm2
         | cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*)
             cvt tm1 $ cvt tm2
         | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg   (*hBOOL*)
         | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
             list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
         | cvt (t as Metis.Term.Fn (x, [])) =
-           (case strip_prefix_and_undo_ascii const_prefix x of
+           (case strip_prefix_and_unascii const_prefix x of
                 SOME c => Const (smart_invert_const c, dummyT)
               | NONE => (*Not a constant. Is it a fixed variable??*)
-            case strip_prefix_and_undo_ascii fixed_var_prefix x of
+            case strip_prefix_and_unascii fixed_var_prefix x of
                 SOME v => Free (v, dummyT)
               | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
                   hol_term_from_metis_PT ctxt t))
         | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis.Term.toString t);
             hol_term_from_metis_PT ctxt t)

             handle Option =>
                 (trace_msg (fn() => "List.find failed for the variable " ^ x ^
                                        " in " ^ Display.string_of_thm ctxt i_th);
                  NONE)
       fun remove_typeinst (a, t) =
-            case strip_prefix_and_undo_ascii schematic_var_prefix a of
+            case strip_prefix_and_unascii schematic_var_prefix a of
                 SOME b => SOME (b, t)
-              | NONE   => case strip_prefix_and_undo_ascii tvar_prefix a of
+              | NONE => case strip_prefix_and_unascii tvar_prefix a of
                 SOME _ => NONE          (*type instantiations are forbidden!*)
-              | NONE   => SOME (a,t)    (*internal Metis var?*)
+              | NONE => SOME (a,t)    (*internal Metis var?*)
       val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
       val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
       val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
       val tms = rawtms |> map (reveal_skolem_terms skolems) |> infer_types ctxt
       val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)