--- a/src/HOL/Tools/Function/function_core.ML Fri Nov 13 20:41:29 2009 +0100
+++ b/src/HOL/Tools/Function/function_core.ML Fri Nov 13 21:11:15 2009 +0100
@@ -456,7 +456,7 @@
let
val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
lthy
- |> LocalTheory.conceal
+ |> Local_Theory.conceal
|> Inductive.add_inductive_i
{quiet_mode = true,
verbose = ! trace,
@@ -470,7 +470,7 @@
[] (* no parameters *)
(map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
[] (* no special monos *)
- ||> LocalTheory.restore_naming lthy
+ ||> Local_Theory.restore_naming lthy
val cert = cterm_of (ProofContext.theory_of lthy)
fun requantify orig_intro thm =
@@ -518,7 +518,7 @@
$ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
|> Syntax.check_term lthy
in
- LocalTheory.define ""
+ Local_Theory.define ""
((Binding.name (function_name fname), mixfix),
((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
end
@@ -928,7 +928,7 @@
PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
val (_, lthy) =
- LocalTheory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
+ Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
val newthy = ProofContext.theory_of lthy
val clauses = map (transfer_clause_ctx newthy) clauses