# HG changeset patch # User wenzelm # Date 1395508509 -3600 # Node ID b72e0a9d62b983161fbfe5e6ad94cb7368ce0b79 # Parent 73e2e1912571c3ea269c61210c97b470833d0b4c more antiquotations; diff -r 73e2e1912571 -r b72e0a9d62b9 src/HOL/Library/bnf_decl.ML --- a/src/HOL/Library/bnf_decl.ML Sat Mar 22 18:12:08 2014 +0100 +++ b/src/HOL/Library/bnf_decl.ML Sat Mar 22 18:15:09 2014 +0100 @@ -94,7 +94,7 @@ val bnf_decl = prepare_decl (K I) (K I); -fun read_constraint _ NONE = HOLogic.typeS +fun read_constraint _ NONE = @{sort type} | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s; val bnf_decl_cmd = prepare_decl read_constraint Syntax.read_typ; diff -r 73e2e1912571 -r b72e0a9d62b9 src/HOL/Library/refute.ML --- a/src/HOL/Library/refute.ML Sat Mar 22 18:12:08 2014 +0100 +++ b/src/HOL/Library/refute.ML Sat Mar 22 18:15:09 2014 +0100 @@ -579,7 +579,7 @@ Type ("fun", [@{typ nat}, @{typ nat}])])) => t | Const (@{const_name Groups.times}, Type ("fun", [@{typ nat}, Type ("fun", [@{typ nat}, @{typ nat}])])) => t - | Const (@{const_name List.append}, _) => t + | Const (@{const_name append}, _) => t (* UNSOUND | Const (@{const_name lfp}, _) => t | Const (@{const_name gfp}, _) => t @@ -684,11 +684,11 @@ and collect_type_axioms T axs = case T of (* simple types *) - Type ("prop", []) => axs - | Type ("fun", [T1, T2]) => collect_type_axioms T2 (collect_type_axioms T1 axs) + Type (@{type_name prop}, []) => axs + | Type (@{type_name fun}, [T1, T2]) => collect_type_axioms T2 (collect_type_axioms T1 axs) | Type (@{type_name set}, [T1]) => collect_type_axioms T1 axs (* axiomatic type classes *) - | Type ("itself", [T1]) => collect_type_axioms T1 axs + | Type (@{type_name itself}, [T1]) => collect_type_axioms T1 axs | Type (s, Ts) => (case Datatype.get_info thy s of SOME _ => (* inductive datatype *) @@ -761,7 +761,7 @@ | Const (@{const_name Groups.times}, T as Type ("fun", [@{typ nat}, Type ("fun", [@{typ nat}, @{typ nat}])])) => collect_type_axioms T axs - | Const (@{const_name List.append}, T) => collect_type_axioms T axs + | Const (@{const_name append}, T) => collect_type_axioms T axs (* UNSOUND | Const (@{const_name lfp}, T) => collect_type_axioms T axs | Const (@{const_name gfp}, T) => collect_type_axioms T axs @@ -819,8 +819,8 @@ val thy = Proof_Context.theory_of ctxt fun collect_types T acc = (case T of - Type ("fun", [T1, T2]) => collect_types T1 (collect_types T2 acc) - | Type ("prop", []) => acc + Type (@{type_name fun}, [T1, T2]) => collect_types T1 (collect_types T2 acc) + | Type (@{type_name prop}, []) => acc | Type (@{type_name set}, [T1]) => collect_types T1 acc | Type (s, Ts) => (case Datatype.get_info thy s of @@ -2620,11 +2620,12 @@ fun List_append_interpreter ctxt model args t = case t of - Const (@{const_name List.append}, Type ("fun", [Type ("List.list", [T]), Type ("fun", - [Type ("List.list", [_]), Type ("List.list", [_])])])) => + Const (@{const_name append}, + Type (@{type_name fun}, [Type (@{type_name list}, [T]), + Type (@{type_name fun}, [Type (@{type_name list}, [_]), Type (@{type_name list}, [_])])])) => let val size_elem = size_of_type ctxt model T - val size_list = size_of_type ctxt model (Type ("List.list", [T])) + val size_list = size_of_type ctxt model (Type (@{type_name list}, [T])) (* maximal length of lists; 0 if we only consider the empty list *) val list_length = let @@ -2866,7 +2867,7 @@ in SOME (fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) pairs HOLogic_empty_set) end - | Type ("prop", []) => + | Type (@{type_name prop}, []) => (case index_from_interpretation intr of ~1 => SOME (HOLogic.mk_Trueprop (Const (@{const_name undefined}, HOLogic.boolT))) | 0 => SOME (HOLogic.mk_Trueprop @{term True}) diff -r 73e2e1912571 -r b72e0a9d62b9 src/HOL/Library/simps_case_conv.ML --- a/src/HOL/Library/simps_case_conv.ML Sat Mar 22 18:12:08 2014 +0100 +++ b/src/HOL/Library/simps_case_conv.ML Sat Mar 22 18:15:09 2014 +0100 @@ -152,13 +152,12 @@ fun was_split t = let - val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq - o fst o HOLogic.dest_imp + val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq o fst o HOLogic.dest_imp val get_conjs = HOLogic.dest_conj o HOLogic.dest_Trueprop - fun dest_alls (Const ("HOL.All", _) $ Abs (_, _, t)) = dest_alls t + fun dest_alls (Const (@{const_name All}, _) $ Abs (_, _, t)) = dest_alls t | dest_alls t = t in forall (is_free_eq_imp o dest_alls) (get_conjs t) end - handle TERM _ => false + handle TERM _ => false fun apply_split ctxt split thm = Seq.of_list let val ((_,thm'), ctxt') = Variable.import false [thm] ctxt in diff -r 73e2e1912571 -r b72e0a9d62b9 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sat Mar 22 18:12:08 2014 +0100 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sat Mar 22 18:15:09 2014 +0100 @@ -999,15 +999,15 @@ val is = upto (1, arity) |> map Int.toString - val arg_tys = map (fn i => TFree ("arg" ^ i ^ "_ty", HOLogic.typeS)) is - val res_ty = TFree ("res" ^ "_ty", HOLogic.typeS) + val arg_tys = map (fn i => TFree ("arg" ^ i ^ "_ty", @{sort type})) is + val res_ty = TFree ("res" ^ "_ty", @{sort type}) val f_ty = arg_tys ---> res_ty val f = Free ("f", f_ty) val xs = map (fn i => - Free ("x" ^ i, TFree ("arg" ^ i ^ "_ty", HOLogic.typeS))) is + Free ("x" ^ i, TFree ("arg" ^ i ^ "_ty", @{sort type}))) is (*FIXME DRY principle*) val ys = map (fn i => - Free ("y" ^ i, TFree ("arg" ^ i ^ "_ty", HOLogic.typeS))) is + Free ("y" ^ i, TFree ("arg" ^ i ^ "_ty", @{sort type}))) is val hyp_lhs = list_comb (f, xs) val hyp_rhs = list_comb (f, ys) @@ -1018,7 +1018,7 @@ |> HOLogic.mk_Trueprop fun conc_eq i = let - val ty = TFree ("arg" ^ i ^ "_ty", HOLogic.typeS) + val ty = TFree ("arg" ^ i ^ "_ty", @{sort type}) val x = Free ("x" ^ i, ty) val y = Free ("y" ^ i, ty) val eq = HOLogic.eq_const ty $ x $ y