1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Mar 06 10:11:38 2014 +0100
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Mar 06 10:12:47 2014 +0100
1.3 @@ -430,7 +430,7 @@
1.4 | NONE => [ax])
1.5
1.6 fun external_frees t =
1.7 - [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
1.8 + [] |> Term.add_frees t |> filter_out (Name.is_internal o fst)
1.9
1.10 fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
1.11 if Config.get ctxt instantiate_inducts then
2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 06 10:11:38 2014 +0100
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 06 10:12:47 2014 +0100
2.3 @@ -144,7 +144,7 @@
2.4 val do_preplay = preplay_timeout <> Time.zeroTime
2.5 val compress_isar = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress_isar
2.6
2.7 - val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
2.8 + val is_fixed = Variable.is_declared ctxt orf Name.is_skolem
2.9 fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
2.10
2.11 fun get_role keep_role ((num, _), role, t, rule, _) =
3.1 --- a/src/Pure/Isar/proof_context.ML Thu Mar 06 10:11:38 2014 +0100
3.2 +++ b/src/Pure/Isar/proof_context.ML Thu Mar 06 10:12:47 2014 +0100
3.3 @@ -427,9 +427,9 @@
3.4 (* check Skolem constants *)
3.5
3.6 fun no_skolem internal x =
3.7 - if can Name.dest_skolem x then
3.8 + if Name.is_skolem x then
3.9 error ("Illegal reference to internal Skolem constant: " ^ quote x)
3.10 - else if not internal andalso can Name.dest_internal x then
3.11 + else if not internal andalso Name.is_internal x then
3.12 error ("Illegal reference to internal variable: " ^ quote x)
3.13 else x;
3.14
3.15 @@ -520,7 +520,7 @@
3.16 (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
3.17 (SOME x, false) =>
3.18 (Context_Position.report ctxt pos
3.19 - (Markup.name x (if can Name.dest_skolem x then Markup.skolem else Markup.free));
3.20 + (Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free));
3.21 Free (x, infer_type ctxt (x, ty)))
3.22 | _ => prep_const_proper ctxt strict (c, pos))
3.23 end;
3.24 @@ -1375,7 +1375,7 @@
3.25 if x = x' then Pretty.str x
3.26 else Pretty.block [Pretty.str x, Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')];
3.27 val fixes =
3.28 - filter_out ((can Name.dest_internal orf member (op =) structs) o #1)
3.29 + filter_out ((Name.is_internal orf member (op =) structs) o #1)
3.30 (Variable.dest_fixes ctxt);
3.31 val prt_fixes =
3.32 if null fixes then []
4.1 --- a/src/Pure/Syntax/syntax_phases.ML Thu Mar 06 10:11:38 2014 +0100
4.2 +++ b/src/Pure/Syntax/syntax_phases.ML Thu Mar 06 10:12:47 2014 +0100
4.3 @@ -51,7 +51,7 @@
4.4 [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c];
4.5
4.6 fun markup_free ctxt x =
4.7 - [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
4.8 + [if Name.is_skolem x then Markup.skolem else Markup.free] @
4.9 (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x
4.10 then [Variable.markup_fixed ctxt x]
4.11 else []);
4.12 @@ -664,7 +664,7 @@
4.13 if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
4.14 then Markup.fixed x else Markup.intensify;
4.15 in
4.16 - if can Name.dest_skolem x
4.17 + if Name.is_skolem x
4.18 then ([m, Markup.skolem], Variable.revert_fixed ctxt x)
4.19 else ([m, Markup.free], x)
4.20 end;
5.1 --- a/src/Pure/Syntax/syntax_trans.ML Thu Mar 06 10:11:38 2014 +0100
5.2 +++ b/src/Pure/Syntax/syntax_trans.ML Thu Mar 06 10:12:47 2014 +0100
5.3 @@ -124,7 +124,7 @@
5.4 | lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts);
5.5
5.6 fun absfree_proper (x, T) t =
5.7 - if can Name.dest_internal x
5.8 + if Name.is_internal x
5.9 then error ("Illegal internal variable in abstraction: " ^ quote x)
5.10 else absfree (x, T) t;
5.11
5.12 @@ -316,7 +316,7 @@
5.13 val body = body_of tm;
5.14 val rev_new_vars = Term.rename_wrt_term body vars;
5.15 fun subst (x, T) b =
5.16 - if can Name.dest_internal x andalso not (Term.is_dependent b)
5.17 + if Name.is_internal x andalso not (Term.is_dependent b)
5.18 then (Const ("_idtdummy", T), incr_boundvars ~1 b)
5.19 else (mark_bound_abs (x, T), Term.subst_bound (mark_bound_body (x, T), b));
5.20 val (rev_vars', body') = fold_map subst rev_new_vars body;
6.1 --- a/src/Pure/name.ML Thu Mar 06 10:11:38 2014 +0100
6.2 +++ b/src/Pure/name.ML Thu Mar 06 10:12:47 2014 +0100
6.3 @@ -13,8 +13,10 @@
6.4 val is_bound: string -> bool
6.5 val internal: string -> string
6.6 val dest_internal: string -> string
6.7 + val is_internal: string -> bool
6.8 val skolem: string -> string
6.9 val dest_skolem: string -> string
6.10 + val is_skolem: string -> bool
6.11 val clean_index: string * int -> string * int
6.12 val clean: string -> string
6.13 type context
6.14 @@ -63,9 +65,11 @@
6.15
6.16 val internal = suffix "_";
6.17 val dest_internal = unsuffix "_";
6.18 +val is_internal = String.isSuffix "_";
6.19
6.20 val skolem = suffix "__";
6.21 val dest_skolem = unsuffix "__";
6.22 +val is_skolem = String.isSuffix "__";
6.23
6.24 fun clean_index (x, i) =
6.25 (case try dest_internal x of
7.1 --- a/src/Pure/variable.ML Thu Mar 06 10:11:38 2014 +0100
7.2 +++ b/src/Pure/variable.ML Thu Mar 06 10:12:47 2014 +0100
7.3 @@ -399,7 +399,7 @@
7.4 fun add_fixes_binding bs ctxt =
7.5 let
7.6 val _ =
7.7 - (case filter (can Name.dest_skolem o Binding.name_of) bs of
7.8 + (case filter (Name.is_skolem o Binding.name_of) bs of
7.9 [] => ()
7.10 | bads => error ("Illegal internal Skolem constant(s): " ^ commas (map Binding.print bads)));
7.11 val _ =
7.12 @@ -417,7 +417,7 @@
7.13 fun variant_fixes raw_xs ctxt =
7.14 let
7.15 val names = names_of ctxt;
7.16 - val xs = map (fn x => Name.clean x |> can Name.dest_internal x ? Name.internal) raw_xs;
7.17 + val xs = map (fn x => Name.clean x |> Name.is_internal x ? Name.internal) raw_xs;
7.18 val (xs', names') = fold_map Name.variant xs names |>> (is_body ctxt ? map Name.skolem);
7.19 in ctxt |> new_fixes names' xs xs' (replicate (length xs) Position.none) end;
7.20