# HG changeset patch # User wenzelm # Date 1394097167 -3600 # Node ID bb21b380f65d17ca307d82343350ed2c91293eec # Parent 72db54a67152d4e8a8d785706f54137ee3600133 tuned signature; diff -r 72db54a67152 -r bb21b380f65d src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Mar 06 10:11:38 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Mar 06 10:12:47 2014 +0100 @@ -430,7 +430,7 @@ | NONE => [ax]) fun external_frees t = - [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst) + [] |> Term.add_frees t |> filter_out (Name.is_internal o fst) fun maybe_instantiate_inducts ctxt hyp_ts concl_t = if Config.get ctxt instantiate_inducts then diff -r 72db54a67152 -r bb21b380f65d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 06 10:11:38 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 06 10:12:47 2014 +0100 @@ -144,7 +144,7 @@ val do_preplay = preplay_timeout <> Time.zeroTime val compress_isar = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress_isar - val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem + val is_fixed = Variable.is_declared ctxt orf Name.is_skolem fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev fun get_role keep_role ((num, _), role, t, rule, _) = diff -r 72db54a67152 -r bb21b380f65d src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Mar 06 10:11:38 2014 +0100 +++ b/src/Pure/Isar/proof_context.ML Thu Mar 06 10:12:47 2014 +0100 @@ -427,9 +427,9 @@ (* check Skolem constants *) fun no_skolem internal x = - if can Name.dest_skolem x then + if Name.is_skolem x then error ("Illegal reference to internal Skolem constant: " ^ quote x) - else if not internal andalso can Name.dest_internal x then + else if not internal andalso Name.is_internal x then error ("Illegal reference to internal variable: " ^ quote x) else x; @@ -520,7 +520,7 @@ (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of (SOME x, false) => (Context_Position.report ctxt pos - (Markup.name x (if can Name.dest_skolem x then Markup.skolem else Markup.free)); + (Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free)); Free (x, infer_type ctxt (x, ty))) | _ => prep_const_proper ctxt strict (c, pos)) end; @@ -1375,7 +1375,7 @@ if x = x' then Pretty.str x else Pretty.block [Pretty.str x, Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')]; val fixes = - filter_out ((can Name.dest_internal orf member (op =) structs) o #1) + filter_out ((Name.is_internal orf member (op =) structs) o #1) (Variable.dest_fixes ctxt); val prt_fixes = if null fixes then [] diff -r 72db54a67152 -r bb21b380f65d src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Thu Mar 06 10:11:38 2014 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Thu Mar 06 10:12:47 2014 +0100 @@ -51,7 +51,7 @@ [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c]; fun markup_free ctxt x = - [if can Name.dest_skolem x then Markup.skolem else Markup.free] @ + [if Name.is_skolem x then Markup.skolem else Markup.free] @ (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x then [Variable.markup_fixed ctxt x] else []); @@ -664,7 +664,7 @@ if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt then Markup.fixed x else Markup.intensify; in - if can Name.dest_skolem x + if Name.is_skolem x then ([m, Markup.skolem], Variable.revert_fixed ctxt x) else ([m, Markup.free], x) end; diff -r 72db54a67152 -r bb21b380f65d src/Pure/Syntax/syntax_trans.ML --- a/src/Pure/Syntax/syntax_trans.ML Thu Mar 06 10:11:38 2014 +0100 +++ b/src/Pure/Syntax/syntax_trans.ML Thu Mar 06 10:12:47 2014 +0100 @@ -124,7 +124,7 @@ | lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts); fun absfree_proper (x, T) t = - if can Name.dest_internal x + if Name.is_internal x then error ("Illegal internal variable in abstraction: " ^ quote x) else absfree (x, T) t; @@ -316,7 +316,7 @@ val body = body_of tm; val rev_new_vars = Term.rename_wrt_term body vars; fun subst (x, T) b = - if can Name.dest_internal x andalso not (Term.is_dependent b) + if Name.is_internal x andalso not (Term.is_dependent b) then (Const ("_idtdummy", T), incr_boundvars ~1 b) else (mark_bound_abs (x, T), Term.subst_bound (mark_bound_body (x, T), b)); val (rev_vars', body') = fold_map subst rev_new_vars body; diff -r 72db54a67152 -r bb21b380f65d src/Pure/name.ML --- a/src/Pure/name.ML Thu Mar 06 10:11:38 2014 +0100 +++ b/src/Pure/name.ML Thu Mar 06 10:12:47 2014 +0100 @@ -13,8 +13,10 @@ val is_bound: string -> bool val internal: string -> string val dest_internal: string -> string + val is_internal: string -> bool val skolem: string -> string val dest_skolem: string -> string + val is_skolem: string -> bool val clean_index: string * int -> string * int val clean: string -> string type context @@ -63,9 +65,11 @@ val internal = suffix "_"; val dest_internal = unsuffix "_"; +val is_internal = String.isSuffix "_"; val skolem = suffix "__"; val dest_skolem = unsuffix "__"; +val is_skolem = String.isSuffix "__"; fun clean_index (x, i) = (case try dest_internal x of diff -r 72db54a67152 -r bb21b380f65d src/Pure/variable.ML --- a/src/Pure/variable.ML Thu Mar 06 10:11:38 2014 +0100 +++ b/src/Pure/variable.ML Thu Mar 06 10:12:47 2014 +0100 @@ -399,7 +399,7 @@ fun add_fixes_binding bs ctxt = let val _ = - (case filter (can Name.dest_skolem o Binding.name_of) bs of + (case filter (Name.is_skolem o Binding.name_of) bs of [] => () | bads => error ("Illegal internal Skolem constant(s): " ^ commas (map Binding.print bads))); val _ = @@ -417,7 +417,7 @@ fun variant_fixes raw_xs ctxt = let val names = names_of ctxt; - val xs = map (fn x => Name.clean x |> can Name.dest_internal x ? Name.internal) raw_xs; + val xs = map (fn x => Name.clean x |> Name.is_internal x ? Name.internal) raw_xs; val (xs', names') = fold_map Name.variant xs names |>> (is_body ctxt ? map Name.skolem); in ctxt |> new_fixes names' xs xs' (replicate (length xs) Position.none) end;