# HG changeset patch # User wenzelm # Date 1145996621 -7200 # Node ID 29bc35832a779a341fecfad53aa1b2a467f47f63 # Parent e6093a7fa53afa2d5a1baaff2f17db4275f70ebe tuned; diff -r e6093a7fa53a -r 29bc35832a77 src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Tue Apr 25 22:23:30 2006 +0200 +++ b/src/Pure/Isar/ROOT.ML Tue Apr 25 22:23:41 2006 +0200 @@ -36,10 +36,10 @@ use "calculation.ML"; use "obtain.ML"; use "locale.ML"; +use "../axclass.ML"; use "local_theory.ML"; use "specification.ML"; use "constdefs.ML"; -use "../axclass.ML"; (*outer syntax*) use "antiquote.ML"; diff -r e6093a7fa53a -r 29bc35832a77 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Tue Apr 25 22:23:30 2006 +0200 +++ b/src/Pure/Isar/element.ML Tue Apr 25 22:23:41 2006 +0200 @@ -326,12 +326,11 @@ let val thy = ProofContext.theory_of ctxt; val th = Goal.norm_hhf raw_th; - val maxidx = #maxidx (Thm.rep_thm th); fun standard_thesis t = let val C = ObjectLogic.drop_judgment thy (Thm.concl_of th); - val C' = Var ((AutoBind.thesisN, maxidx + 1), Term.fastype_of C); + val C' = Var ((AutoBind.thesisN, Thm.maxidx_of th + 1), Term.fastype_of C); in Term.subst_atomic [(C, C')] t end; val raw_prop = diff -r e6093a7fa53a -r 29bc35832a77 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Tue Apr 25 22:23:30 2006 +0200 +++ b/src/Pure/Proof/extraction.ML Tue Apr 25 22:23:41 2006 +0200 @@ -101,7 +101,7 @@ in get_first (fn (_, (prems, (tm1, tm2))) => let - fun ren t = getOpt (Term.rename_abs tm1 tm t, t); + fun ren t = the_default t (Term.rename_abs tm1 tm t); val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1); val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty); val prems' = map (pairself (Envir.subst_vars env o inc o ren)) prems; @@ -463,7 +463,7 @@ val procs = List.concat (map (fst o snd) types); val rtypes = map fst types; val typroc = typeof_proc (Sign.defaultS thy'); - val prep = getOpt (prep, K I) thy' o ProofRewriteRules.elim_defs thy' false defs o + val prep = the_default (K I) prep thy' o ProofRewriteRules.elim_defs thy' false defs o Reconstruct.expand_proof thy' (("", NONE) :: map (apsnd SOME) expand); val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns); diff -r e6093a7fa53a -r 29bc35832a77 src/Pure/Proof/proof_rewrite_rules.ML --- a/src/Pure/Proof/proof_rewrite_rules.ML Tue Apr 25 22:23:30 2006 +0200 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Tue Apr 25 22:23:41 2006 +0200 @@ -231,7 +231,7 @@ val (_, rhs) = Logic.dest_equals prop; val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts) (foldr (fn p => Abs ("", dummyT, abstract_over p)) rhs vs), - map valOf ts); + map the ts); in change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs' end diff -r e6093a7fa53a -r 29bc35832a77 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Tue Apr 25 22:23:30 2006 +0200 +++ b/src/Pure/Tools/codegen_package.ML Tue Apr 25 22:23:41 2006 +0200 @@ -164,7 +164,7 @@ NameSpace.drop_base c'; val c'' = NameSpace.append prefix (NameSpace.base c'); fun mangle (Type (tyco, tys)) = - (NameSpace.base o alias_get thy) tyco :: Library.flat (List.mapPartial mangle tys) |> SOME + (NameSpace.base o alias_get thy) tyco :: flat (List.mapPartial mangle tys) |> SOME | mangle _ = NONE in @@ -172,7 +172,7 @@ |> Type.raw_match (Sign.the_const_type thy c, ty) |> map (snd o snd) o Vartab.dest |> List.mapPartial mangle - |> Library.flat + |> flat |> null ? K ["x"] |> cons c'' |> space_implode "_" @@ -959,7 +959,7 @@ in map_atyps (fn _ => ty_inst) ty end; val tys = (Type.logical_types o Sign.tsig_of) thy - |> filter (fn tyco => (is_some oo try) (Sorts.mg_domain (Sign.classes_of thy, Sign.arities_of thy) tyco) (Sign.defaultS thy)) + |> filter (fn tyco => can (Sign.arity_sorts thy tyco) (Sign.defaultS thy)) |> map inst in (overltab1 @@ -1027,7 +1027,7 @@ then I else cons (name, NameSpace.append thyname (NameSpace.base name))) names []; in diff names end; - val inconsistent = map get_inconsistent (ThyInfo.names ()) |> Library.flat; + val inconsistent = map get_inconsistent (ThyInfo.names ()) |> flat; fun add (src, dst) thy = if (is_some oo Symtab.lookup o fst o #alias o #logic_data o CodegenData.get) thy src then (warning ("code generator alias already defined for " ^ quote src ^ ", will not overwrite"); thy) diff -r e6093a7fa53a -r 29bc35832a77 src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Tue Apr 25 22:23:30 2006 +0200 +++ b/src/Pure/Tools/codegen_serializer.ML Tue Apr 25 22:23:41 2006 +0200 @@ -892,7 +892,7 @@ in vs |> map (fn (v, sort) => map (pair v) sort) - |> Library.flat + |> flat |> from_sctxt end; fun hs_from_tycoexpr fxy (tyco, tys) = diff -r e6093a7fa53a -r 29bc35832a77 src/Pure/Tools/codegen_theorems.ML --- a/src/Pure/Tools/codegen_theorems.ML Tue Apr 25 22:23:30 2006 +0200 +++ b/src/Pure/Tools/codegen_theorems.ML Tue Apr 25 22:23:41 2006 +0200 @@ -441,7 +441,7 @@ of [] => Defs.specifications_of (Theory.defs_of thy) c |> map (PureThy.get_thms thy o Name o fst o snd) - |> Library.flat + |> flat |> append (getf_first_list (map (fn f => f thy) (the_funs_extrs thy)) (c, ty)) |> map (dest_fun thy) |> filter_typ diff -r e6093a7fa53a -r 29bc35832a77 src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Tue Apr 25 22:23:30 2006 +0200 +++ b/src/Pure/Tools/codegen_thingol.ML Tue Apr 25 22:23:41 2006 +0200 @@ -715,7 +715,7 @@ (the_default empty_module o Option.map dest_modl o try (Graph.get_node modl2)) name) and diff_modl prefix (modl1, modl2) = fold (diff_entry prefix modl2) - ((AList.make (Graph.get_node modl1) o Library.flat o Graph.strong_conn) modl1) + ((AList.make (Graph.get_node modl1) o flat o Graph.strong_conn) modl1) in diff_modl [] modl12 [] end; local @@ -768,7 +768,7 @@ |> imports [] name (*|> cons name |> map (fn name => submodules name (get_modl name) []) - |> Library.flat + |> flat |> remove (op =) name*) |> map NameSpace.pack end;